Analysis I, Section 8.3: Uncountable sets #

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Uncountable sets.

Some non-trivial API is provided beyond what is given in the textbook in order connect these notions with existing summation notions.

source

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

¬EqualCard X (Set X)

Theorem 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 ℕ)

Corollary 8.3.3

source

theorem Chapter8.Uncountable.real :

Uncountable ℝ

Corollary 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

Exercise 8.3.2. Some subtle type changes due to how sets are implemented in Mathlib. Also we shift the sequence D by one so that we can work in Set A rather than Set B.

source

@[reducible, inline]

abbrev Chapter8.LeCard (X Y : Type) :

Prop

Equations