Analysis I, Section 8.1: Countability

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:

• Custom notions for "equal cardinality", "countable", and "at most countable". Note that Mathlib's Countable.{u} (α : Sort u) : PropCountable typeclass corresponds to what we call "at most countable" in this text.

• Countability of the integers and rationals.

Note that as the Chapter 3 set theory has been deprecated, we will not re-use relevant constructions from that theory here, replacing them with Mathlib counterparts instead.

namespace Chapter8 theorem declaration uses 'sorry'EqualCard.refl (X : Type) : EqualCard X X := sorrytheorem declaration uses 'sorry'EqualCard.symm {X Y : Type} (hXY : EqualCard X Y) : EqualCard Y X := byX:TypeY:TypehXY:EqualCard X Y⊢ EqualCard Y X sorryAll goals completed! 🐙theorem declaration uses 'sorry'EqualCard.trans {X Y Z : Type} (hXY : EqualCard X Y) (hYZ : EqualCard Y Z) : EqualCard X Z := byX:TypeY:TypeZ:TypehXY:EqualCard X YhYZ:EqualCard Y Z⊢ EqualCard X Z sorryAll goals completed! 🐙instance EqualCard.instSetoid : Setoid Type := ⟨ EqualCard, ⟨ refl, symm, trans ⟩ ⟩theorem EqualCard.univ (X : Type) : EqualCard (.univ : Set X) X := ⟨ Subtype.val, Subtype.val_injective, byX:Type⊢ Function.Surjective Subtype.val intro _X:Typeb✝:X⊢ ∃ a, ↑a = b✝; aesopAll goals completed! 🐙 ⟩abbrev CountablyInfinite (X : Type) : Prop := EqualCard X ℕabbrev AtMostCountable (X : Type) : Prop := CountablyInfinite X ∨ Finite Xtheorem CountablyInfinite.equiv {X Y: Type} (hXY : EqualCard X Y) : CountablyInfinite X ↔ CountablyInfinite Y := ⟨ hXY.symm.trans, hXY.trans ⟩theorem Finite.equiv {X Y: Type} (hXY : EqualCard X Y) : Finite X ↔ Finite Y := byX:TypeY:TypehXY:EqualCard X Y⊢ Finite X ↔ Finite Y obtain ⟨ f, hf ⟩ := hXYintroX:TypeY:Typef:X → Yhf:Function.Bijective f⊢ Finite X ↔ Finite Y; exact (Equiv.ofBijective f hf).finite_iffAll goals completed! 🐙theorem AtMostCountable.equiv {X Y: Type} (hXY : EqualCard X Y) : AtMostCountable X ↔ AtMostCountable Y := byX:TypeY:TypehXY:EqualCard X Y⊢ AtMostCountable X ↔ AtMostCountable Y simp [AtMostCountable, CountablyInfinite.equiv hXY, Finite.equiv hXY]All goals completed! 🐙 theorem CountablyInfinite.toCountable {X : Type} (hX: CountablyInfinite X) : Countable X := byX:TypehX:CountablyInfinite X⊢ Countable X simp_all [iff']All goals completed! 🐙theorem CountablyInfinite.toInfinite {X : Type} (hX: CountablyInfinite X) : Infinite X := byX:TypehX:CountablyInfinite X⊢ Infinite X simp_all [iff']All goals completed! 🐙theorem AtMostCountable.iff (X : Type) : AtMostCountable X ↔ Countable X := byX:Type⊢ AtMostCountable X ↔ Countable X observe h1 : CountablyInfinite X ↔ Countable X ∧ Infinite XX:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite X⊢ AtMostCountable X ↔ Countable X observe h2 : Finite X ∨ Infinite XX:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite Xh2:Finite X ∨ Infinite X⊢ AtMostCountable X ↔ Countable X observe h3 : Finite X → Countable XX:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite Xh2:Finite X ∨ Infinite Xh3:Finite X → Countable X⊢ AtMostCountable X ↔ Countable X tautoAll goals completed! 🐙theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite X ↔ ∃ f : ℕ ↪ A, X = f '' .univ := byA:TypeX:Set A⊢ CountablyInfinite ↑X ↔ ∃ f, X = ⇑f '' Set.univ constructormpA:TypeX:Set A⊢ CountablyInfinite ↑X → ∃ f, X = ⇑f '' Set.univmprA:TypeX:Set A⊢ (∃ f, X = ⇑f '' Set.univ) → CountablyInfinite ↑X .mpA:TypeX:Set A⊢ CountablyInfinite ↑X → ∃ f, X = ⇑f '' Set.univ intro ⟨ g, hg ⟩mpA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective g⊢ ∃ f, X = ⇑f '' Set.univ choose f hleft hright using Function.bijective_iff_has_inverse.mp hgmpA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ ∃ f, X = ⇑f '' Set.univ refine ⟨ ⟨ Subtype.val ∘ f, ?_ ⟩, ?_ ⟩mp.refine_1A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ Function.Injective (Subtype.val ∘ f)mp.refine_2A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ X = ⇑{ toFun := Subtype.val ∘ f, inj' := ?mp.refine_1 } '' Set.univ .mp.refine_1A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ Function.Injective (Subtype.val ∘ f) intro x y hxymp.refine_1A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx:ℕy:ℕhxy:(Subtype.val ∘ f) x = (Subtype.val ∘ f) y⊢ x = y; apply hright.injectivemp.refine_1.aA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx:ℕy:ℕhxy:(Subtype.val ∘ f) x = (Subtype.val ∘ f) y⊢ f x = f y; simp_all [Subtype.val_inj]All goals completed! 🐙 extmp.refine_2.hA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X ↔ x✝ ∈ ⇑{ toFun := Subtype.val ∘ f, inj' := ⋯ } '' Set.univ; simpmp.refine_2.hA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X ↔ ∃ y, ↑(f y) = x✝; constructormp.refine_2.h.mpA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X → ∃ y, ↑(f y) = x✝mp.refine_2.h.mprA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ (∃ y, ↑(f y) = x✝) → x✝ ∈ X .mp.refine_2.h.mpA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X → ∃ y, ↑(f y) = x✝ intro hxmp.refine_2.h.mpA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:Ahx:x✝ ∈ X⊢ ∃ y, ↑(f y) = x✝; use g ⟨ _, hx ⟩hA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:Ahx:x✝ ∈ X⊢ ↑(f (g ⟨x✝, hx⟩)) = x✝; simp [hleft _]All goals completed! 🐙 rintro ⟨ _, rfl ⟩mp.refine_2.h.mpr.introA:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gw✝:ℕ⊢ ↑(f w✝) ∈ X; aesopAll goals completed! 🐙 intro ⟨ f, hf ⟩mprA:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univ⊢ CountablyInfinite ↑X have := Function.leftInverse_invFun (Function.Embedding.injective f)mprA:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)⊢ CountablyInfinite ↑X use (Function.invFun f) ∘ Subtype.valhA:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)⊢ Function.Bijective (Function.invFun ⇑f ∘ Subtype.val); split_andsh.refine_1A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)⊢ Function.Injective (Function.invFun ⇑f ∘ Subtype.val)h.refine_2A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)⊢ Function.Surjective (Function.invFun ⇑f ∘ Subtype.val) .h.refine_1A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)⊢ Function.Injective (Function.invFun ⇑f ∘ Subtype.val) rintro ⟨ x, hx ⟩ ⟨ y, hy ⟩ hh.refine_1.mk.mkA:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)x:Ahx:x ∈ Xy:Ahy:y ∈ Xh:(Function.invFun ⇑f ∘ Subtype.val) ⟨x, hx⟩ = (Function.invFun ⇑f ∘ Subtype.val) ⟨y, hy⟩⊢ ⟨x, hx⟩ = ⟨y, hy⟩; grindAll goals completed! 🐙 intro nh.refine_2A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:?_mvar.133034 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)n:ℕ⊢ ∃ a, (Function.invFun ⇑f ∘ Subtype.val) a = n; use ⟨ f n, byA:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑_fvar.132963) ⇑_fvar.132963 := Function.leftInverse_invFun (Function.Embedding.injective _fvar.132963)n:ℕ⊢ f n ∈ X aesopAll goals completed! 🐙 ⟩; grindAll goals completed! 🐙 declaration uses 'sorry'example : CountablyInfinite (.univ \ {0}: Set ℕ) := by⊢ CountablyInfinite ↑(Set.univ \ {0}) sorryAll goals completed! 🐙declaration uses 'sorry'example : CountablyInfinite ((fun n:ℕ ↦ 2*n) '' .univ) := by⊢ CountablyInfinite ↑((fun n => 2 * n) '' Set.univ) sorryAll goals completed! 🐙 def declaration uses 'sorry'Int.exists_unique_min : Decidable (∀ (X : Set ℤ) (hX : X.Nonempty), ∃! m ∈ X, ∀ n ∈ X, m ≤ n) := by⊢ Decidable (∀ (X : Set ℤ), X.Nonempty → ∃! m, m ∈ X ∧ ∀ n ∈ X, m ≤ n) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙def declaration uses 'sorry'NNRat.exists_unique_min : Decidable (∀ (X : Set NNRat) (hX : X.Nonempty), ∃! m ∈ X, ∀ n ∈ X, m ≤ n) := by⊢ Decidable (∀ (X : Set ℚ≥0), X.Nonempty → ∃! m, m ∈ X ∧ ∀ n ∈ X, m ≤ n) -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙open Classical in noncomputable abbrev Nat.min (X : Set ℕ) : ℕ := if hX : X.Nonempty then (exists_unique_min hX).exists.choose else 0theorem Nat.min_spec {X : Set ℕ} (hX : X.Nonempty) : min X ∈ X ∧ ∀ n ∈ X, min X ≤ n := byX:Set ℕhX:X.Nonempty⊢ min X ∈ X ∧ ∀ n ∈ X, min X ≤ n simp [hX, min]X:Set ℕhX:X.Nonempty⊢ ⋯.choose ∈ X ∧ ∀ n ∈ X, ⋯.choose ≤ n; exact (exists_unique_min hX).exists.choose_specAll goals completed! 🐙theorem Nat.min_eq {X : Set ℕ} (hX : X.Nonempty) {a:ℕ} (ha : a ∈ X ∧ ∀ n ∈ X, a ≤ n) : min X = a := (exists_unique_min hX).unique (min_spec hX) ha@[simp] theorem Nat.min_empty : min ∅ = 0 := by⊢ min ∅ = 0 simp [Nat.min]All goals completed! 🐙declaration uses 'sorry'example : Nat.min ((fun n ↦ 2*n) '' (.Ici 1)) = 2 := by⊢ Nat.min ((fun n => 2 * n) '' Set.Ici 1) = 2 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Nat.min_eq_sInf {X : Set ℕ} (hX : X.Nonempty) : min X = sInf X := byX:Set ℕhX:X.Nonempty⊢ min X = sInf X sorryAll goals completed! 🐙open Classical in /-- Equivalence with Mathlib's `Nat.find` method -/ theorem Nat.min_eq_find {X : Set ℕ} (hX : X.Nonempty) : min X = Nat.find hX := byX:Set ℕhX:X.Nonempty⊢ min X = Nat.find hX symmX:Set ℕhX:X.Nonempty⊢ Nat.find hX = min X; rw [Nat.find_eq_iff]X:Set ℕhX:X.Nonempty⊢ min X ∈ X ∧ ∀ n < min X, n ∉ X; have := min_spec hXX:Set ℕhX:X.Nonemptythis:?_mvar.142721 := Chapter8.Nat.min_spec _fvar.141846⊢ min X ∈ X ∧ ∀ n < min X, n ∉ X; grindAll goals completed! 🐙 theorem Nat.countable_of_infinite (X : Set ℕ) [Infinite X] : CountablyInfinite X := byX:Set ℕinst✝:Infinite ↑X⊢ CountablyInfinite ↑X have := (monotone_enum_of_infinite X).existsX:Set ℕinst✝:Infinite ↑Xthis:?_mvar.167918 := ExistsUnique.exists (Chapter8.Nat.monotone_enum_of_infinite _fvar.167914)⊢ CountablyInfinite ↑X exact EqualCard.symm ⟨ this.choose, this.choose_spec.1 ⟩All goals completed! 🐙 theorem AtMostCountable.subset' {A: Type} {X Y: Set A} (hX: AtMostCountable X) (hY: Y ⊆ X) : AtMostCountable Y := byA:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ AtMostCountable ↑Y refine' (equiv ⟨ fun y ↦ ⟨ ↑↑y, y.property ⟩, _, _ ⟩).mp (subset hX { x : X | ↑x ∈ Y })refine'_1A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Injective fun y => ⟨↑↑y, ⋯⟩refine'_2A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Surjective fun y => ⟨↑↑y, ⋯⟩ .refine'_1A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Injective fun y => ⟨↑↑y, ⋯⟩ intro ⟨ ⟨ _, _ ⟩, _ ⟩ ⟨ ⟨ _, _ ⟩, _ ⟩ _refine'_1A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ Xval✝¹:Aproperty✝³:val✝¹ ∈ Xproperty✝²:⟨val✝¹, property✝³⟩ ∈ {x | ↑x ∈ Y}val✝:Aproperty✝¹:val✝ ∈ Xproperty✝:⟨val✝, property✝¹⟩ ∈ {x | ↑x ∈ Y}a✝:(fun y => ⟨↑↑y, ⋯⟩) ⟨⟨val✝¹, property✝³⟩, property✝²⟩ = (fun y => ⟨↑↑y, ⋯⟩) ⟨⟨val✝, property✝¹⟩, property✝⟩⊢ ⟨⟨val✝¹, property✝³⟩, property✝²⟩ = ⟨⟨val✝, property✝¹⟩, property✝⟩; simp_allAll goals completed! 🐙 intro ⟨ y, hy ⟩refine'_2A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ Xy:Ahy:y ∈ Y⊢ ∃ a, (fun y => ⟨↑↑y, ⋯⟩) a = ⟨y, hy⟩; use ⟨ ⟨ y, hY hy ⟩, byA:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ Xy:Ahy:y ∈ Y⊢ ⟨y, ⋯⟩ ∈ {x | ↑x ∈ Y} aesopAll goals completed! 🐙 ⟩ theorem declaration uses 'sorry'explicit_bijection_spec : Function.Bijective explicit_bijection := by⊢ Function.Bijective explicit_bijection sorryAll goals completed! 🐙end Chapter8