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

Theorem 8.3.1

theorem Chapter8.Uncountable.iff (X : Type) : Uncountable X ↔ ¬AtMostCountable X

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

theorem Chapter8.Uncountable.power_set_nat : Uncountable (Set ℕ)

Corollary 8.3.3

theorem Chapter8.Uncountable.real : Uncountable ℝ

Corollary 8.3.4

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.

@[reducible, inline]

abbrev Chapter8.LeCard (X Y : Type) : Prop

Equations

• Chapter8.LeCard X Y = ∃ (f : X → Y), Function.Injective f

theorem Chapter8.Schroder_Bernstein {X Y : Type} (hXY : LeCard X Y) (hYX : LeCard Y X) : EqualCard X Y

Exercise 8.3.3

@[reducible, inline]

abbrev Chapter8.LtCard (X Y : Type) : Prop

Equations

• Chapter8.LtCard X Y = (Chapter8.LeCard X Y ∧ ¬Chapter8.EqualCard X Y)

@[reducible, inline]

abbrev Chapter8.CardOrder : Preorder Type

Equations

• Chapter8.CardOrder = { le := Chapter8.LeCard, lt := Chapter8.LtCard, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }