4. 집합과 함수
집합, 관계, 함수의 어휘는 수학의 모든 분야에서 구성을 수행하기 위한 통일된 언어를 제공합니다. 함수와 관계는 집합을 이용해 정의할 수 있으므로, 공리적 집합론을 수학의 기초로 사용할 수 있습니다.
반면 Lean의 기초는 타입이라는 원시 개념에 기반을 두며, 타입 사이의 함수를 정의하는 방법을 포함합니다. Lean의 모든 표현식은 타입을 가집니다. 자연수, 실수, 실수에서 실수로 가는 함수, 군, 벡터 공간 등이 있습니다. 어떤 표현식은 그 자체가 타입입니다. 다시 말해, 그 표현식의 타입이 Type입니다. Lean과 Mathlib은 새로운 타입을 정의하는 방법과 그 타입의 대상을 정의하는 방법을 제공합니다.
개념적으로는 타입을 단순히 대상들의 집합으로 생각해도 됩니다. 모든 대상이 타입을 갖도록 요구하면 몇 가지 이점이 있습니다. 예를 들어 +와 같은 표기를 오버로드할 수 있고, Lean이 대상의 타입으로부터 많은 정보를 추론할 수 있으므로 입력이 덜 장황해지는 경우도 있습니다. 또한 타입 시스템 덕분에 Lean은 함수에 잘못된 개수의 인자를 적용하거나 잘못된 타입의 인자를 적용했을 때 오류를 표시할 수 있습니다.
Lean의 라이브러리는 기초적인 집합론 개념을 실제로 정의하고 있습니다. 집합론과 달리 Lean에서 집합은 항상 어떤 타입의 대상들로 이루어진 집합입니다. 예를 들어 자연수의 집합이나 실수에서 실수로 가는 함수들의 집합이 그렇습니다. 타입과 집합의 구분에 익숙해지려면 시간이 다소 걸리지만, 이 장에서 핵심적인 내용을 차근차근 안내하겠습니다.
4.1. 집합
α가 임의의 타입이면, Set α 타입은 α의 원소들로 이루어진 집합들로 구성됩니다. 이 타입은 일반적인 집합론적 연산과 관계를 지원합니다. 예를 들어, s ⊆ t는 s가 t의 부분집합임을 뜻하고, s ∩ t는 s와 t의 교집합을, s ∪ t는 두 집합의 합집합을 나타냅니다. 부분집합 관계는 \ss 또는 \sub로, 교집합은 \i 또는 \cap으로, 합집합은 \un 또는 \cup으로 입력할 수 있습니다. 라이브러리는 또한 α 타입의 모든 원소로 이루어진 집합 univ와, \empty로 입력할 수 있는 공집합 ∅도 정의합니다. x : α와 s : Set α가 주어졌을 때, 표현식 x ∈ s는 x가 s의 원소임을 뜻합니다. 집합의 원소 관계를 언급하는 정리는 이름에 mem을 포함하는 경우가 많습니다. 표현식 x ∉ s는 ¬ x ∈ s의 축약형입니다. ∈는 \in 또는 \mem으로, ∉는 \notin으로 입력할 수 있습니다.
집합에 관한 사실을 증명하는 한 가지 방법은 rw나 단순화기(simplifier)를 사용해 정의를 펼치는 것입니다. 아래 두 번째 예제에서는 simp only를 사용하여, 단순화기가 전체 항등식 데이터베이스가 아니라 우리가 제공한 항등식 목록만 사용하도록 지시합니다. rw와 달리, simp는 전칭 한정기호나 존재 한정기호 안에서도 단순화를 수행할 수 있습니다. 증명을 한 단계씩 따라가 보면 이 명령들의 효과를 확인할 수 있습니다.
variable {α : Type*}
variable (s t u : Set α)
open Set
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
rw [subset_def, inter_def, inter_def]
rw [subset_def] at h
simp only [mem_setOf]
rintro x ⟨xs, xu⟩
exact ⟨h _ xs, xu⟩
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
simp only [subset_def, mem_inter_iff] at *
rintro x ⟨xs, xu⟩
exact ⟨h _ xs, xu⟩
이 예제에서는 정리들의 더 짧은 이름을 사용하기 위해 Set 네임스페이스를 엽니다. 하지만 사실 rw와 simp 호출은 완전히 지워도 됩니다:
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
intro x xsu
exact ⟨h xsu.1, xsu.2⟩
여기서 일어나는 일을 정의적 환원(definitional reduction)이라고 합니다. intro 명령과 익명 생성자를 이해하기 위해 Lean은 정의를 펼칠 수밖에 없습니다. 다음 예제도 이 현상을 보여 줍니다:
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
fun _x ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩
합집합을 다룰 때는 Set.union_def와 Set.mem_union을 사용할 수 있습니다. x ∈ s ∪ t는 x ∈ s ∨ x ∈ t로 펼쳐지므로, cases 택틱을 사용하여 정의적 환원을 강제할 수도 있습니다.
example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
intro x hx
have xs : x ∈ s := hx.1
have xtu : x ∈ t ∪ u := hx.2
rcases xtu with xt | xu
· left
show x ∈ s ∩ t
exact ⟨xs, xt⟩
· right
show x ∈ s ∩ u
exact ⟨xs, xu⟩
교집합은 합집합보다 더 강하게 결합하므로 표현식 (s ∩ t) ∪ (s ∩ u)에서 괄호는 필요 없지만, 괄호를 쓰면 표현식의 의미가 더 명확해집니다. 다음은 같은 사실에 대한 더 짧은 증명입니다:
example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
rintro x ⟨xs, xt | xu⟩
· left; exact ⟨xs, xt⟩
· right; exact ⟨xs, xu⟩
연습 삼아 반대 방향의 포함 관계를 증명해 보십시오:
example : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
sorry
rintro를 사용할 때 Lean이 논리합 패턴 h1 | h2를 올바르게 파싱하도록 하려면 그 패턴을 괄호로 감싸야 할 때가 있다는 점을 알아 두면 도움이 될 것입니다.
라이브러리는 차집합 s \ t도 정의합니다. 여기서 백슬래시는 \\로 입력하는 특수 유니코드 문자입니다. 표현식 x ∈ s \ t는 x ∈ s ∧ x ∉ t로 전개됩니다. (∉는 \notin으로 입력할 수 있습니다.) Set.diff_eq와 dsimp, 또는 Set.mem_diff를 사용하여 직접 다시 쓸 수도 있지만, 다음에 나오는 같은 포함 관계에 대한 두 증명은 이들을 사용하지 않는 방법을 보여 줍니다.
example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
intro x xstu
have xs : x ∈ s := xstu.1.1
have xnt : x ∉ t := xstu.1.2
have xnu : x ∉ u := xstu.2
constructor
· exact xs
intro xtu
-- x ∈ t ∨ x ∈ u
rcases xtu with xt | xu
· show False; exact xnt xt
· show False; exact xnu xu
example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
rintro x ⟨⟨xs, xnt⟩, xnu⟩
use xs
rintro (xt | xu) <;> contradiction
연습 삼아 역방향의 포함 관계를 증명하십시오:
example : s \ (t ∪ u) ⊆ (s \ t) \ u := by
sorry
두 집합이 같음을 증명하려면 한 집합의 모든 원소가 다른 집합의 원소임을 보이는 것으로 충분합니다. 이 원리는 “외연성(extensionality)”이라고 알려져 있으며, 당연하게도 ext 택틱이 이를 처리할 수 있습니다.
example : s ∩ t = t ∩ s := by
ext x
simp only [mem_inter_iff]
constructor
· rintro ⟨xs, xt⟩; exact ⟨xt, xs⟩
· rintro ⟨xt, xs⟩; exact ⟨xs, xt⟩
이번에도 simp only [mem_inter_iff] 줄을 지워도 증명에는 아무런 문제가 없습니다. 사실, 난해한 증명 항을 좋아하신다면 다음의 한 줄짜리 증명이 마음에 드실 것입니다:
example : s ∩ t = t ∩ s :=
Set.ext fun _x ↦ ⟨fun ⟨xs, xt⟩ ↦ ⟨xt, xs⟩, fun ⟨xt, xs⟩ ↦ ⟨xs, xt⟩⟩
다음은 단순화기(simplifier)를 사용한 훨씬 더 짧은 증명입니다:
example : s ∩ t = t ∩ s := by ext x; simp [and_comm]
ext를 사용하는 대신 Subset.antisymm 정리를 사용할 수도 있습니다. 이 정리를 사용하면 s ⊆ t와 t ⊆ s를 증명하여 집합 사이의 등식 s = t를 증명할 수 있습니다.
example : s ∩ t = t ∩ s := by
apply Subset.antisymm
· rintro x ⟨xs, xt⟩; exact ⟨xt, xs⟩
· rintro x ⟨xt, xs⟩; exact ⟨xs, xt⟩
이 증명 항을 완성해 보십시오:
example : s ∩ t = t ∩ s :=
Subset.antisymm sorry sorry
sorry를 밑줄로 바꿀 수 있으며, 그 위에 마우스를 올리면 Lean이 그 지점에서 무엇을 기대하는지 보여 준다는 점을 기억하십시오.
다음은 증명해 보면 재미있을 만한 집합론적 항등식들입니다:
example : s ∩ (s ∪ t) = s := by
sorry
example : s ∪ s ∩ t = s := by
sorry
example : s \ t ∪ t = s ∪ t := by
sorry
example : s \ t ∪ t \ s = (s ∪ t) \ (s ∩ t) := by
sorry
집합을 표현하는 방식과 관련하여, 내부에서 실제로 어떤 일이 일어나는지 살펴보겠습니다. 타입 이론에서 타입 α 위의 성질 또는 술어는 단지 함수 P : α → Prop일 뿐입니다. 이는 이치에 맞습니다. a : α가 주어지면 P a는 단지 P가 a에 대해 성립한다는 명제입니다. 라이브러리에서 Set α는 α → Prop으로 정의되고, x ∈ s는 s x로 정의됩니다. 다시 말해, 집합은 실제로는 대상으로 취급되는 성질입니다.
라이브러리는 집합 조건제시법 표기도 정의합니다. 표현식 { y | P y }는 (fun y ↦ P y)로 펼쳐지므로, x ∈ { y | P y }는 P x로 환원됩니다. 따라서 짝수라는 성질을 짝수들의 집합으로 바꿀 수 있습니다:
def evens : Set ℕ :=
{ n | Even n }
def odds : Set ℕ :=
{ n | ¬Even n }
example : evens ∪ odds = univ := by
rw [evens, odds]
ext n
simp [-Nat.not_even_iff_odd]
apply Classical.em
이 증명을 한 단계씩 따라가면서 무슨 일이 일어나는지 이해했는지 확인하십시오. 목표에 ¬ Even n을 그대로 두어야 하므로 단순화기(simplifier)에게 보조정리 Nat.not_even_iff를 사용하지 않도록 지시한다는 점에 유의하십시오. rw [evens, odds] 줄을 삭제해 보고 증명이 여전히 작동하는지 확인하십시오.
사실 조건제시법 표기는 다음을 정의하는 데 사용됩니다
s ∩ t는{x | x ∈ s ∧ x ∈ t}로,s ∪ t는{x | x ∈ s ∨ x ∈ t}로,∅은{x | False}로, 그리고univ는{x | True}로 정의됩니다.
Lean은 우리가 어느 것을 의미하는지 추측하기 어려워하기 때문에, ∅과 univ의 타입을 명시적으로 지정해야 하는 경우가 많습니다. 다음 예제들은 필요할 때 Lean이 마지막 두 정의를 어떻게 펼치는지 보여 줍니다. 두 번째 예제에서 trivial은 라이브러리에 있는 True의 표준 증명입니다.
example (x : ℕ) (h : x ∈ (∅ : Set ℕ)) : False :=
h
example (x : ℕ) : x ∈ (univ : Set ℕ) :=
trivial
연습 문제로, 다음 포함 관계를 증명하십시오. intro n을 사용하여 부분집합의 정의를 펼치고, 단순화기(simplifier)를 사용하여 집합론적 구성을 논리로 환원하십시오. Nat.Prime.eq_two_or_odd와 Nat.odd_iff 정리를 사용하는 것도 권장합니다.
example : { n | Nat.Prime n } ∩ { n | n > 2 } ⊆ { n | ¬Even n } := by
sorry
주의하십시오. 라이브러리에 술어 Prime의 버전이 여러 개 있다는 점은 다소 혼란스럽습니다. 가장 일반적인 것은 영 원소를 갖는 모든 가환 모노이드에서 의미가 있습니다. 술어 Nat.Prime은 자연수에 특화되어 있습니다. 다행히 이 특정한 경우에는 두 개념이 일치한다는 정리가 있으므로, 언제든지 한쪽을 다른 쪽으로 재작성할 수 있습니다.
#print Prime
#print Nat.Prime
example (n : ℕ) : Prime n ↔ Nat.Prime n :=
Nat.prime_iff.symm
example (n : ℕ) (h : Prime n) : Nat.Prime n := by
rw [Nat.prime_iff]
exact h
rwa 택틱은 재작성을 한 뒤 assumption 택틱을 적용하여 가정으로 목표를 닫습니다.
example (n : ℕ) (h : Prime n) : Nat.Prime n := by
rwa [Nat.prime_iff]
Lean은 ∀ x ∈ s, ...라는 표기법을 도입합니다. 이는 “s에 속하는 모든 x에 대해 …,”라는 뜻이며 ∀ x, x ∈ s → ...의 약어입니다. 또한 “s에 속하는 x가 존재하여 ..”라는 뜻의 ∃ x ∈ s, ..., 표기도 도입합니다. 이 구성은 한정기호의 의미를 집합 s로 제한하는 역할을 하므로, 이들을 유계 한정기호라고 부르기도 합니다. 그래서 라이브러리에서 이들을 사용하는 정리의 이름에는 ball이나 bex가 들어 있는 경우가 많습니다. 정리 bex_def는 ∃ x ∈ s, ...가 ∃ x, x ∈ s ∧ ...,와 동치임을 주장하지만, rintro, use, 익명 생성자와 함께 사용할 때는 이 두 표현식이 거의 똑같이 동작합니다. 따라서 보통은 bex_def를 사용하여 이들을 명시적으로 변환할 필요가 없습니다. 다음은 이들을 사용하는 몇 가지 예입니다:
variable (s t : Set ℕ)
example (h₀ : ∀ x ∈ s, ¬Even x) (h₁ : ∀ x ∈ s, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
intro x xs
constructor
· apply h₀ x xs
apply h₁ x xs
example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ s, Prime x := by
rcases h with ⟨x, xs, _, prime_x⟩
use x, xs
다음과 같이 약간 변형된 명제들을 증명할 수 있는지 확인해 보십시오:
section
variable (ssubt : s ⊆ t)
example (h₀ : ∀ x ∈ t, ¬Even x) (h₁ : ∀ x ∈ t, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
sorry
example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ t, Prime x := by
sorry
end
첨자가 붙은 합집합과 교집합은 또 하나의 중요한 집합론적 구성입니다. α의 원소들로 이루어진 집합들의 수열 \(A_0, A_1, A_2, \ldots\)를 함수 A : ℕ → Set α로 모델링할 수 있습니다. 이 경우 ⋃ i, A i는 이들의 합집합을, ⋂ i, A i는 이들의 교집합을 나타냅니다. 여기서 자연수가 특별한 역할을 하는 것은 아니므로, ℕ을 집합들의 첨자로 쓰이는 임의의 타입 I로 바꿀 수 있습니다. 다음은 이들의 사용법을 보여 줍니다.
variable {α I : Type*}
variable (A B : I → Set α)
variable (s : Set α)
open Set
example : (s ∩ ⋃ i, A i) = ⋃ i, A i ∩ s := by
ext x
simp only [mem_inter_iff, mem_iUnion]
constructor
· rintro ⟨xs, ⟨i, xAi⟩⟩
exact ⟨i, xAi, xs⟩
rintro ⟨i, xAi, xs⟩
exact ⟨xs, ⟨i, xAi⟩⟩
example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ ⋂ i, B i := by
ext x
simp only [mem_inter_iff, mem_iInter]
constructor
· intro h
constructor
· intro i
exact (h i).1
intro i
exact (h i).2
rintro ⟨h1, h2⟩ i
constructor
· exact h1 i
exact h2 i
첨자가 붙은 합집합이나 교집합에는 괄호가 자주 필요한데, 한정기호와 마찬가지로 속박 변수의 범위가 가능한 한 멀리까지 확장되기 때문입니다.
다음 항등식을 증명해 보십시오. 한쪽 방향은 고전 논리가 필요합니다! 증명의 적절한 지점에서 by_cases xs : x ∈ s를 사용하는 것을 권장합니다.
example : (s ∪ ⋂ i, A i) = ⋂ i, A i ∪ s := by
sorry
Mathlib에는 유계 한정기호와 유사한 유계 합집합과 유계 교집합도 있습니다. mem_iUnion₂와 mem_iInter₂로 그 의미를 풀어 볼 수 있습니다. 다음 예제에서 볼 수 있듯이, Lean의 단순화기도 이러한 치환을 수행합니다.
def primes : Set ℕ :=
{ x | Nat.Prime x }
example : (⋃ p ∈ primes, { x | p ^ 2 ∣ x }) = { x | ∃ p ∈ primes, p ^ 2 ∣ x } :=by
ext
rw [mem_iUnion₂]
simp
example : (⋃ p ∈ primes, { x | p ^ 2 ∣ x }) = { x | ∃ p ∈ primes, p ^ 2 ∣ x } := by
ext
simp
example : (⋂ p ∈ primes, { x | ¬p ∣ x }) ⊆ { x | x = 1 } := by
intro x
contrapose!
simp
apply Nat.exists_prime_and_dvd
이와 비슷한 다음 예제를 풀어 보십시오. eq_univ를 입력하기 시작하면, 탭 자동 완성 기능이 apply eq_univ_of_forall이 증명을 시작하기에 좋은 방법이라고 알려 줄 것입니다. 정리 Nat.exists_infinite_primes를 사용하는 것도 권장합니다.
example : (⋃ p ∈ primes, { x | x ≤ p }) = univ := by
sorry
집합들의 모임 s : Set (Set α)가 주어지면, 그 합집합 ⋃₀ s는 Set α 타입을 가지며 {x | ∃ t ∈ s, x ∈ t}로 정의됩니다. 마찬가지로, 그 교집합 ⋂₀ s는 {x | ∀ t ∈ s, x ∈ t}로 정의됩니다. 이 연산들은 각각 sUnion과 sInter라고 부릅니다. 다음 예제들은 이 연산들과 유계 합집합 및 유계 교집합 사이의 관계를 보여 줍니다.
variable {α : Type*} (s : Set (Set α))
example : ⋃₀ s = ⋃ t ∈ s, t := by
ext x
rw [mem_iUnion₂]
simp
example : ⋂₀ s = ⋂ t ∈ s, t := by
ext x
rw [mem_iInter₂]
rfl
라이브러리에서 이 항등식들은 sUnion_eq_biUnion과 sInter_eq_biInter라고 부릅니다.
4.2. 함수
f : α → β가 함수이고 p가 타입 β의 원소들의 집합이면, 라이브러리는 preimage f p를 {x | f x ∈ p}로 정의하며, 이를 f ⁻¹' p로 표기합니다. 표현식 x ∈ f ⁻¹' p는 f x ∈ p로 환원됩니다. 다음 예제에서처럼, 이는 종종 편리합니다.
variable {α β : Type*}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)
open Function
open Set
example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by
ext
rfl
s가 타입 α의 원소들의 집합이면, 라이브러리는 image f s도 {y | ∃ x, x ∈ s ∧ f x = y}로 정의하며, 이를 f '' s로 표기합니다. 따라서 가설 y ∈ f '' s는 삼중쌍 ⟨x, xs, xeq⟩로 분해되며, 여기서 x : α는 가설 xs : x ∈ s와 xeq : f x = y를 만족합니다. rintro 택틱의 rfl 태그(제 3.2 절 참조)는 바로 이러한 상황을 위해 만들어졌습니다.
example : f '' (s ∪ t) = f '' s ∪ f '' t := by
ext y; constructor
· rintro ⟨x, xs | xt, rfl⟩
· left
use x, xs
right
use x, xt
rintro (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩)
· use x, Or.inl xs
use x, Or.inr xt
또한 use 택틱은 가능한 경우 rfl을 적용하여 목표를 닫는다는 점에 주목하십시오.
다음은 또 다른 예제입니다.
example : s ⊆ f ⁻¹' (f '' s) := by
intro x xs
show f x ∈ f '' s
use x, xs
그 목적을 위해 특별히 설계된 정리를 사용하고 싶다면 use x, xs 줄을 apply mem_image_of_mem f xs로 바꿀 수 있습니다. 하지만 상이 존재 한정기호를 사용하여 정의된다는 것을 알아 두면 편리한 경우가 많습니다.
다음 동치는 좋은 연습 문제입니다.
example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
sorry
이는 image f와 preimage f가 각각 부분집합 관계로 부분 순서가 주어진 Set α와 Set β 사이의 이른바 갈루아 연결(Galois connection)의 한 예임을 보여 줍니다. 라이브러리에서 이 동치는 image_subset_iff라는 이름으로 되어 있습니다. 실제로는 우변이 더 유용한 표현인 경우가 많습니다. x ∈ f ⁻¹' t는 f x ∈ t로 펼쳐지는 반면, y ∈ f '' s를 다루려면 존재 한정기호를 분해해야 하기 때문입니다.
다음은 여러분이 즐길 수 있는 집합론적 항등식의 긴 목록입니다. 한꺼번에 모두 풀 필요는 없습니다. 몇 개만 풀고 나머지는 나중을 위해 남겨 두십시오.
example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by
sorry
example : f '' (f ⁻¹' u) ⊆ u := by
sorry
example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
sorry
example (h : s ⊆ t) : f '' s ⊆ f '' t := by
sorry
example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by
sorry
example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by
sorry
example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
sorry
example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by
sorry
example : f '' s \ f '' t ⊆ f '' (s \ t) := by
sorry
example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) := by
sorry
example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by
sorry
example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := by
sorry
example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by
sorry
example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by
sorry
다음 연습 문제군에도 도전해 보십시오. 이 문제들은 첨자가 붙은 합집합 및 교집합에 대해 상과 역상이 어떻게 동작하는지를 다룹니다. 세 번째 연습문제에서는 첨자 집합이 공집합이 아님을 보장하기 위해 인자 i : I가 필요합니다. 이들 중 어느 것을 증명하든, ext나 intro를 사용하여 집합 사이의 등식이나 포함 관계의 의미를 펼친 다음, simp를 호출하여 원소 조건을 풀어내기를 권장합니다.
variable {I : Type*} (A : I → Set α) (B : I → Set β)
example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
sorry
example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
sorry
example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
sorry
example : (f ⁻¹' ⋃ i, B i) = ⋃ i, f ⁻¹' B i := by
sorry
example : (f ⁻¹' ⋂ i, B i) = ⋂ i, f ⁻¹' B i := by
sorry
라이브러리는 f가 s 위에서 단사임을 나타내기 위해 술어 InjOn f s를 정의합니다. 그 정의는 다음과 같습니다:
example : InjOn f s ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ s, f x₁ = f x₂ → x₁ = x₂ :=
Iff.refl _
Injective f라는 명제는 InjOn f univ와 동치임을 증명할 수 있습니다. 마찬가지로 라이브러리는 range f를 {x | ∃y, f y = x}로 정의하므로, range f가 f '' univ와 같음을 증명할 수 있습니다. 이는 Mathlib에서 흔히 볼 수 있는 패턴입니다. 함수의 많은 성질이 정의역 전체를 기준으로 정의되지만, 명제를 정의역 타입의 부분집합으로 제한한 상대화된 버전이 함께 있는 경우가 많습니다.
다음은 InjOn과 range를 사용하는 몇 가지 예입니다.
open Set Real
example : InjOn log { x | x > 0 } := by
intro x xpos y ypos e
calc
x = exp (log x) := by rw [exp_log xpos]
_ = exp (log y) := by rw [e]
_ = y := by rw [exp_log ypos]
example : range exp = { y | y > 0 } := by
ext y; constructor
· rintro ⟨x, rfl⟩
apply exp_pos
intro ypos
use log y
rw [exp_log ypos]
다음을 증명해 보십시오.
example : InjOn sqrt { x | x ≥ 0 } := by
sorry
example : InjOn (fun x ↦ x ^ 2) { x : ℝ | x ≥ 0 } := by
sorry
example : sqrt '' { x | x ≥ 0 } = { y | y ≥ 0 } := by
sorry
example : (range fun x ↦ x ^ 2) = { y : ℝ | y ≥ 0 } := by
sorry
함수 f : α → β의 역함수를 정의하기 위해 두 가지 새로운 요소를 사용하겠습니다. 첫째, Lean에서는 임의의 타입이 비어 있을 수 있다는 사실을 처리해야 합니다. f x = y를 만족하는 x가 없을 때 y에서 f의 역함수 값을 정의하려면 α의 기본값을 할당해야 합니다. [Inhabited α] 표기를 변수로 추가하는 것은 α에 특별히 지정된 원소가 있다고 가정하는 것과 같으며, 이 원소는 default로 표기됩니다. 둘째, f x = y를 만족하는 x가 둘 이상인 경우 역함수는 그중 하나를 선택해야 합니다. 이를 위해서는 선택 공리에 의존해야 합니다. Lean에서는 선택 공리를 여러 방법으로 사용할 수 있습니다. 편리한 방법 중 하나는 아래에서 보듯이 고전적인 choose 연산자를 사용하는 것입니다.
variable {α β : Type*} [Inhabited α]
#check (default : α)
variable (P : α → Prop) (h : ∃ x, P x)
#check Classical.choose h
example : P (Classical.choose h) :=
Classical.choose_spec h
h : ∃ x, P x가 주어지면, Classical.choose h의 값은 P x를 만족하는 어떤 x입니다. 정리 Classical.choose_spec h는 Classical.choose h가 이 명세를 만족한다는 것을 말합니다.
이것들을 갖추면 역함수를 다음과 같이 정의할 수 있습니다:
noncomputable section
open Classical
def inverse (f : α → β) : β → α := fun y : β ↦
if h : ∃ x, f x = y then Classical.choose h else default
theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := by
rw [inverse, dif_pos h]
exact Classical.choose_spec h
고전 논리를 본질적으로 사용하고 있으므로 noncomputable section과 open Classical 줄이 필요합니다. 입력 y에 대해 함수 inverse f는 f x = y를 만족하는 x가 있으면 그러한 x의 값 하나를 반환하고, 없으면 α의 기본 원소를 반환합니다. 참인 경우에 반환되는 값인 Classical.choose h가 가정 h에 의존하므로, 이것은 의존 if 구문의 한 예입니다. 항등식 dif_pos h는 h : e가 주어지면 if h : e then a else b를 a로 다시 쓰고, 마찬가지로 dif_neg h는 h : ¬ e가 주어지면 이를 b로 다시 씁니다. 비의존 if 구문에 쓰이는 if_pos와 if_neg 버전도 있으며, 이들은 다음 절에서 사용됩니다. 정리 inverse_spec은 inverse f가 이 명세의 첫 번째 부분을 만족한다는 것을 말합니다.
이것들이 어떻게 작동하는지 완전히 이해하지 못하더라도 걱정하지 마십시오. inverse_spec 정리만으로도 inverse f가 좌역함수일 필요충분조건은 f가 단사인 것이고, 우역함수일 필요충분조건은 f가 전사인 것임을 충분히 보일 수 있을 것입니다. VS Code에서 LeftInverse와 RightInverse를 더블 클릭하거나 마우스 오른쪽 버튼으로 클릭하여, 또는 #print LeftInverse와 #print RightInverse 명령을 사용하여 이들의 정의를 찾아보십시오. 그런 다음 두 정리를 증명해 보십시오. 이 증명들은 까다롭습니다! 세부 사항을 하나하나 파고들기 전에 먼저 종이 위에서 증명해 보면 도움이 됩니다. 각각을 여섯 줄 정도의 짧은 줄로 증명할 수 있을 것입니다. 추가적인 도전을 원한다면 각 증명을 한 줄짜리 증명 항으로 압축해 보십시오.
variable (f : α → β)
open Function
example : Injective f ↔ LeftInverse (inverse f) f :=
sorry
example : Surjective f ↔ RightInverse (inverse f) f :=
sorry
이 절은 집합에서 그 멱집합으로 가는 전사 함수가 존재하지 않는다는 칸토어의 유명한 정리를 타입 이론적으로 진술한 명제로 마무리합니다. 증명을 이해할 수 있는지 살펴본 다음, 빠져 있는 두 줄을 채워 보십시오.
theorem Cantor : ∀ f : α → Set α, ¬Surjective f := by
intro f surjf
let S := { i | i ∉ f i }
rcases surjf S with ⟨j, h⟩
have h₁ : j ∉ f j := by
intro h'
have : j ∉ f j := by rwa [h] at h'
contradiction
have h₂ : j ∈ S
sorry
have h₃ : j ∉ S
sorry
contradiction
4.3. 슈뢰더-베른슈타인 정리
이 장은 집합론의 기초적이지만 자명하지 않은 정리 하나로 마무리합니다. \(\alpha\)와 \(\beta\)를 집합이라고 합시다. (우리의 형식화에서는 이들이 실제로 타입이 됩니다.) \(f : \alpha → \beta\)와 \(g : \beta → \alpha\)가 모두 단사라고 가정합시다. 직관적으로 이는 \(\alpha\)가 \(\beta\)보다 크지 않고, 그 반대도 마찬가지라는 뜻입니다. \(\alpha\)와 \(\beta\)가 유한하다면, 이로부터 둘의 기수가 같다는 결론이 나오며, 이는 둘 사이에 전단사가 존재한다고 말하는 것과 동치입니다. 19세기에 칸토어는 \(\alpha\)와 \(\beta\)가 무한한 경우에도 같은 결과가 성립한다고 주장했습니다. 이는 결국 데데킨트, 슈뢰더, 베른슈타인에 의해 각각 독립적으로 증명되었습니다.
이 형식화에서는 이후 장들에서 더 자세히 설명할 몇 가지 새로운 방법을 소개합니다. 여기서 그 방법들이 너무 빠르게 지나가더라도 걱정하지 마십시오. 우리의 목표는 여러분이 실제 수학적 결과의 형식적 증명에 기여할 수 있는 역량을 이미 갖추고 있음을 보여 드리는 것입니다.
증명의 바탕에 있는 아이디어를 이해하기 위해, \(\alpha\) 안에서 사상 \(g\)의 상을 생각해 봅시다. 그 상 위에서는 \(g\)의 역함수가 정의되며, 이는 \(\beta\)와의 전단사입니다.
문제는 이 전단사가 그림의 음영 영역을 포함하지 않는다는 것입니다. 이 영역은 \(g\)가 전사가 아니면 공집합이 아닙니다. 또는 \(f\)를 사용하여 \(\alpha\) 전체를 \(\beta\)로 보낼 수도 있지만, 이 경우에는 \(f\)가 전사가 아니면 \(\beta\)의 일부 원소를 놓치게 된다는 문제가 있습니다.
하지만 이제 \(\alpha\)에서 자기 자신으로 가는 합성 \(g \circ f\)를 생각해 봅시다. 이 합성은 단사이므로 \(\alpha\)와 그 상 사이의 전단사를 이루며, 그 결과 자기 자신 안에 \(\alpha\)의 축소된 복사본이 생깁니다.
이 합성은 안쪽의 음영 환을 또 다른 그러한 집합으로 보내며, 이 집합은 더 작은 동심 음영 환으로 생각할 수 있고, 이런 식으로 계속 이어집니다. 그 결과 동심 음영 고리들의 수열이 생기며, 각 고리는 다음 고리와 전단사 대응을 이룹니다. 각 환을 다음 환으로 보내고 \(\alpha\)의 음영이 없는 부분은 그대로 두면, \(\alpha\)와 \(g\)의 상 사이의 전단사를 얻습니다. 여기에 \(g^{-1}\)를 합성하면 \(\alpha\)와 \(\beta\) 사이의 원하는 전단사를 얻습니다.
이 전단사를 더 간단하게 기술할 수 있습니다. \(A\)를 음영 영역들로 이루어진 수열의 합집합이라 하고, \(h : \alpha \to \beta\)를 다음과 같이 정의합니다:
다시 말해, 음영 부분에서는 \(f\)를 사용하고 그 밖의 모든 곳에서는 \(g\)의 역함수를 사용합니다. 이렇게 얻은 사상 \(h\)는 각 성분이 단사이고 두 성분의 상이 서로소이므로 단사입니다. 이것이 전사임을 보이기 위해, \(\beta\)의 원소 \(y\)가 주어졌다고 가정하고 \(g(y)\)를 생각해 봅시다. \(g(y)\)가 음영 영역 중 하나에 있다면, 그것은 첫 번째 환형 영역에 있을 수 없으므로 이전 환형 영역에 있는 어떤 \(x\)에 대해 \(g(y) = g(f(x))\)입니다. \(g\)가 단사이므로 \(h(x) = f(x) = y\)가 성립합니다. \(g(y)\)가 음영 영역에 속하지 않는다면, \(h\)의 정의에 의해 \(h(g(y))= y\)가 성립합니다. 어느 경우든 \(y\)는 \(h\)의 상에 속합니다.
이 논증은 그럴듯하게 들리겠지만, 세부 사항은 까다롭습니다. 증명을 형식화하면 결과에 대한 확신이 커질 뿐만 아니라 결과를 더 잘 이해하는 데에도 도움이 됩니다. 이 증명은 고전 논리를 사용하므로, 우리의 정의들이 일반적으로 계산 가능하지 않을 것이라고 Lean에 알려 줍니다.
noncomputable section
open Classical
variable {α β : Type*} [Nonempty β]
[Nonempty β] 표기는 β가 비어 있지 않음을 명시합니다. \(g^{-1}\)를 구성하는 데 사용할 Mathlib 기본 연산이 이를 요구하므로 이 표기를 사용합니다. 정리에서 \(\beta\)가 비어 있는 경우는 자명하며, 그 경우까지 포괄하도록 형식화를 일반화하는 것이 어렵지는 않겠지만 굳이 다루지 않겠습니다. 구체적으로, Mathlib에 정의된 연산 invFun에 가설 [Nonempty β]가 필요합니다. x : α가 주어졌을 때, invFun g x는 β에 x의 역상이 있으면 그중 하나를 고르고, 없으면 β의 임의의 원소를 반환합니다. 함수 invFun g는 g가 단사이면 항상 좌역함수이고, g가 전사이면 항상 우역함수입니다.
#check (invFun g : α → β)
#check (leftInverse_invFun : Injective g → LeftInverse (invFun g) g)
#check (leftInverse_invFun : Injective g → ∀ y, invFun g (g y) = y)
#check (invFun_eq : (∃ y, g y = x) → g (invFun g x) = x)
음영 영역들의 합집합에 해당하는 집합을 다음과 같이 정의합니다.
variable (f : α → β) (g : β → α)
def sbAux : ℕ → Set α
| 0 => univ \ g '' univ
| n + 1 => g '' (f '' sbAux n)
def sbSet :=
⋃ n, sbAux f g n
정의 sbAux는 재귀적 정의의 한 예이며, 이에 대해서는 다음 장에서 설명하겠습니다. 이는 다음과 같은 집합들의 수열을 정의합니다
정의 sbSet은 증명 개요의 집합 \(A = \bigcup_{n \in \mathbb{N}} S_n\)에 대응합니다. 이제 위에서 설명한 함수 \(h\)를 다음과 같이 정의합니다:
def sbFun (x : α) : β :=
if x ∈ sbSet f g then f x else invFun g x
우리가 정의한 \(g^{-1}\)가 \(A\)의 여집합, 즉 \(\alpha\)에서 음영 영역이 아닌 부분에서 우역함수라는 사실이 필요합니다. 이는 가장 바깥쪽 환인 \(S_0\)이 \(\alpha \setminus g(\beta)\)와 같아서 \(A\)의 여집합이 \(g(\beta)\)에 포함되기 때문입니다. 따라서 \(A\)의 여집합에 속하는 모든 \(x\)에 대해 \(g(y) = x\)를 만족하는 \(y\)가 존재합니다. (\(g\)가 단사이므로 이 \(y\)는 유일하지만, 다음 정리는 invFun g x가 g y = x를 만족하는 어떤 y를 반환한다는 것만 말해 줍니다.)
아래 증명을 한 단계씩 따라가며 무슨 일이 일어나는지 이해했는지 확인하고, 나머지 부분을 채우십시오. 마지막에는 invFun_eq를 사용해야 합니다. 여기서 sbAux로 재작성하면 sbAux f g 0이 해당 정의 등식의 우변으로 바뀐다는 점에 주목하십시오.
theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
have : x ∈ g '' univ := by
contrapose! hx
rw [sbSet, mem_iUnion]
use 0
rw [sbAux, mem_sdiff]
sorry
have : ∃ y, g y = x := by
sorry
sorry
이제 \(h\)가 단사임을 증명해 봅시다. 비형식적으로 설명하면 증명은 다음과 같이 진행됩니다. 먼저 \(h(x_1) = h(x_2)\)라고 가정합니다. \(x_1\)이 \(A\)에 속하면 \(h(x_1) = f(x_1)\)이고, 다음과 같이 \(x_2\)도 \(A\)에 속함을 보일 수 있습니다. 그렇지 않다면 \(h(x_2) = g^{-1}(x_2)\)입니다. \(f(x_1) = h(x_1) = h(x_2)\)로부터 \(g(f(x_1)) = x_2\)를 얻습니다. \(A\)의 정의에 따르면 \(x_1\)이 \(A\)에 속하므로 \(x_2\)도 \(A\)에 속하게 되는데, 이는 모순입니다. 따라서 \(x_1\)이 \(A\)에 속하면 \(x_2\)도 \(A\)에 속하며, 이 경우 \(f(x_1) = h(x_1) = h(x_2) = f(x_2)\)가 성립합니다. 그러면 \(f\)가 단사이므로 \(x_1 = x_2\)입니다. 대칭적인 논증으로 \(x_2\)가 \(A\)에 속하면 \(x_1\)도 마찬가지임을 보일 수 있으며, 이로부터 다시 \(x_1 = x_2\)가 따라옵니다.
남은 유일한 가능성은 \(x_1\)도 \(x_2\)도 \(A\)에 속하지 않는 경우입니다. 이 경우 \(g^{-1}(x_1) = h(x_1) = h(x_2) = g^{-1}(x_2)\)가 성립합니다. 양변에 \(g\)를 적용하면 \(x_1 = x_2\)를 얻습니다.
다시 한번, 다음 증명을 한 단계씩 따라가며 이 논증이 Lean에서 어떻게 전개되는지 살펴보시기를 권합니다. sb_right_inv를 사용하여 증명을 마무리할 수 있는지 시도해 보십시오.
theorem sb_injective (hf : Injective f) : Injective (sbFun f g) := by
set A := sbSet f g with A_def
set h := sbFun f g with h_def
intro x₁ x₂ (hxeq : h x₁ = h x₂)
show x₁ = x₂
simp only [h_def, sbFun, ← A_def] at hxeq
by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
· wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA
· symm
apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
have x₂A : x₂ ∈ A := by
apply _root_.not_imp_self.mp
intro (x₂nA : x₂ ∉ A)
rw [if_pos x₁A, if_neg x₂nA] at hxeq
rw [A_def, sbSet, mem_iUnion] at x₁A
have x₂eq : x₂ = g (f x₁) := by
sorry
rcases x₁A with ⟨n, hn⟩
rw [A_def, sbSet, mem_iUnion]
use n + 1
simp [sbAux]
exact ⟨x₁, hn, x₂eq.symm⟩
sorry
push Not at xA
sorry
이 증명에서는 몇 가지 새로운 택틱이 등장합니다. 먼저 set 택틱에 주목하십시오. 이 택틱은 sbSet f g와 sb_fun f g에 대해 각각 A와 h라는 약칭을 도입합니다. 이에 대응하는 정의 등식에는 A_def와 h_def라는 이름을 붙입니다. 이 약칭들은 정의적(definitional)입니다. 즉, Lean은 필요할 때 이들을 자동으로 펼치기도 합니다. 하지만 항상 그런 것은 아닙니다. 예를 들어 rw를 사용할 때는 일반적으로 A_def와 h_def를 명시적으로 사용해야 합니다. 따라서 이러한 정의에는 득실이 있습니다. 표현식을 더 짧고 읽기 쉽게 만들어 주지만, 때로는 우리가 더 많은 작업을 해야 합니다.
더 흥미로운 택틱은 wlog 택틱입니다. 이 택틱은 위의 비형식적 증명에 나온 대칭성 논증을 담아냅니다. 지금은 이에 대해 자세히 다루지 않겠지만, 이 택틱이 우리가 원하는 일을 정확히 수행한다는 점에 주목하십시오. 택틱 위에 마우스를 올리면 해당 문서를 살펴볼 수 있습니다.
전사성에 대한 논증은 훨씬 더 쉽습니다. \(\beta\)에 속하는 \(y\)가 주어지면, \(g(y)\)가 \(A\)에 속하는지 여부에 따라 두 가지 경우를 고려합니다. 그렇다면 그것은 가장 바깥쪽 환인 \(S_0\)에 속할 수 없습니다. 정의에 따라 그 환은 \(g\)의 상과 서로소이기 때문입니다. 따라서 그것은 어떤 \(n\)에 대해 \(S_{n+1}\)의 원소입니다. 이는 그것이 \(S_n\)에 속하는 어떤 \(x\)에 대해 \(g(f(x))\) 꼴이라는 뜻입니다. \(g\)의 단사성에 의해 \(f(x) = y\)를 얻습니다. \(g(y)\)가 \(A\)의 여집합에 속하는 경우에는 곧바로 \(h(g(y))= y\)를 얻으므로 증명이 끝납니다.
다시 한 번, 증명을 한 단계씩 따라가며 빠진 부분을 채워 보시기를 권합니다. rcases n with _ | n 택틱은 g y ∈ sbAux f g 0인 경우와 g y ∈ sbAux f g (n + 1)인 경우로 나눕니다. 두 경우 모두 simp [sbAux]로 단순화기를 호출하면 sbAux의 해당 정의 등식이 적용됩니다.
theorem sb_surjective (hg : Injective g) : Surjective (sbFun f g) := by
set A := sbSet f g with A_def
set h := sbFun f g with h_def
intro y
by_cases gyA : g y ∈ A
· rw [A_def, sbSet, mem_iUnion] at gyA
rcases gyA with ⟨n, hn⟩
rcases n with _ | n
· simp [sbAux] at hn
simp [sbAux] at hn
rcases hn with ⟨x, xmem, hx⟩
use x
have : x ∈ A := by
rw [A_def, sbSet, mem_iUnion]
exact ⟨n, xmem⟩
rw [h_def, sbFun, if_pos this]
apply hg hx
sorry
이제 이 모든 것을 하나로 합칠 수 있습니다. 최종 명제는 짧고 간결하며, 증명에는 Bijective h가 Injective h ∧ Surjective h로 펼쳐진다는 사실이 사용됩니다.
theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) :
∃ h : α → β, Bijective h :=
⟨sbFun f g, sb_injective f g hf, sb_surjective f g hg⟩