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나 간소화기를 사용하여 정의를 펼치는 것입니다. 아래의 두 번째 예제에서는 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⟩
여기서 일어나는 일은 정의적 축약이라고 알려져 있습니다. 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
두 집합이 같음을 증명하려면, 한 집합의 모든 원소가 다른 집합의 원소임을 보이는 것으로 충분합니다. 이 원리는 “외연성”으로 알려져 있으며, 당연하게도 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⟩⟩
다음은 단순화기를 사용한 훨씬 더 짧은 증명입니다.
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
이 증명을 단계별로 살펴보며 무슨 일이 일어나고 있는지 이해해야 합니다. 여기서 단순화기(simplifier)에게 보조정리 Nat.not_even_iff를 사용하지말라고 알려주는 이유는 목표에 ¬ Even n을 유지하고 싶기 때문이라는 점에 유의하십시오. 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을 사용하여 부분집합의 정의를 펼치고, 단순화기를 사용하여 집합론적 구성을 논리로 축소하십시오. 또한 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 → ...의 축약입니다. 또한 Lean은 ∃ x ∈ s, ...,라는 표기법도 도입하는데, 이는 “s안에서 ..인 x가 존재한다”를 뜻합니다. 이것들은 종종 bounded quantifiers라고 불리는데, 이는 이러한 구성이 그 의미를 집합 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를 정의하며, 이는 f ⁻¹' p로 표기되고 {x | f x ∈ 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도 정의하며, 이는 f '' s로 표기되고 {y | ∃ x, x ∈ s ∧ f x = y}입니다. 따라서 가설 y ∈ f '' s는 xs : x ∈ s와 xeq : f x = y라는 가설을 만족하는 x : α를 갖는 삼중항 ⟨x, xs, xeq⟩로 분해됩니다. 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 β 사이의 이른바 갈루아 연결의 한 예임을 보여줍니다. 라이브러리에서 이 동치는 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값이 있으면 그 값을 반환하고, 그렇지 않으면 α의 기본 원소를 반환합니다. 이는 의존적 if 구성의 한 예인데, 긍정적인 경우에 반환되는 값인 Classical.choose h가 가정 h에 의존하기 때문입니다. 항등식 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\)도 그러하며, 이 경우 \(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\)의 상(image)과 서로소이기 때문입니다. 따라서 그것은 어떤 \(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⟩