Аналіз I, Розділ 8.3: Незліченні множини #

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Незліченні множини.

Надано деякий нетривіальний API, який доповнює матеріал підручника і пов'язує ці поняття з наявними поняттями підсумовування.

source

theorem Chapter8.EqualCard.power_set_false (X : Type) :

¬EqualCard X (Set X)

Теорема 8.3.1

source

theorem Chapter8.Uncountable.iff (X : Type) :

Uncountable X ↔ ¬AtMostCountable X

source

theorem Chapter8.Uncountable.equiv {X Y : Type} (hXY : EqualCard X Y) :

Uncountable X ↔ Uncountable Y

source

theorem Chapter8.Uncountable.power_set_nat :

Uncountable (Set ℕ)

Наслідок 8.3.3

source

theorem Chapter8.Uncountable.real :

Uncountable ℝ

Наслідок 8.3.4

source

theorem Chapter8.Schroder_Bernstein_lemma {X : Type} {A B C : Set X} (hAB : A ⊆ B) (hBC : B ⊆ C) (f : ↑C ↪ ↑A) :

have D := fun (t : ℕ) => Nat.rec ((⇑f.image ∘ ⇑(B.embeddingOfSubset C hBC).image) {x : ↑B | ↑x ∉ A}) (fun (x : ℕ) => ⇑f.image ∘ ⇑(B.embeddingOfSubset C hBC).image ∘ ⇑(A.embeddingOfSubset B hAB).image) t; Set.univ.PairwiseDisjoint D ∧ have g := fun (x : ↑A) => if h : x ∈ ⋃ (n : ℕ), D n ∧ ∃ (y : ↑B), f ⟨↑y, ⋯⟩ = x then ⋯.choose else ⟨↑x, ⋯⟩; Function.Bijective g

Вправа 8.3.2. Дещо тонкі зміни типів через спосіб реалізації множин у Mathlib. Також ми зсуваємо послідовність D на одиницю, щоб працювати у Set A замість Set B.

source

@[reducible, inline]

abbrev Chapter8.LeCard (X Y : Type) :

Prop

Equations