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 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.

@[reducible, inline]

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

The definition of equal cardinality. For simplicity we restrict attention to the Type 0 universe. This is analogous to Chapter3.SetTheory.Set.EqualCard, but we are not using the latter since the Chapter 3 set theory is deprecated.

Equations

• Chapter8.EqualCard X Y = ∃ (f : X → Y), Function.Bijective f

theorem Chapter8.EqualCard.iff {X Y : Type} : EqualCard X Y ↔ Nonempty (X ≃ Y)

Relation with Mathlib's Equiv concept

theorem Chapter8.EqualCard.iff' {X Y : Type} : EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y

Equivalence with Mathlib's Cardinal.mk concept

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

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

theorem Chapter8.EqualCard.trans {X Y Z : Type} (hXY : EqualCard X Y) (hYZ : EqualCard Y Z) : EqualCard X Z

instance Chapter8.EqualCard.instSetoid : Setoid Type

Equations

• Chapter8.EqualCard.instSetoid = { r := Chapter8.EqualCard, iseqv := Chapter8.EqualCard.instSetoid._proof_1 }

theorem Chapter8.EqualCard.univ (X : Type) : EqualCard (↑Set.univ) X

@[reducible, inline]

abbrev Chapter8.CountablyInfinite (X : Type) : Prop

Equations

• Chapter8.CountablyInfinite X = Chapter8.EqualCard X ℕ

@[reducible, inline]

abbrev Chapter8.AtMostCountable (X : Type) : Prop

Equations

• Chapter8.AtMostCountable X = (Chapter8.CountablyInfinite X ∨ Finite X)

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

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

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

theorem Chapter8.CountablyInfinite.iff (X : Type) : CountablyInfinite X ↔ Nonempty (Denumerable X)

Equivalence with Mathlib's Denumerable concept (cf. Remark 8.1.2)

theorem Chapter8.CountablyInfinite.iff' (X : Type) : CountablyInfinite X ↔ Countable X ∧ Infinite X

Equivalence with Mathlib's Countable typeclass

theorem Chapter8.CountablyInfinite.toCountable {X : Type} (hX : CountablyInfinite X) : Countable X

theorem Chapter8.CountablyInfinite.toInfinite {X : Type} (hX : CountablyInfinite X) : Infinite X

theorem Chapter8.AtMostCountable.iff (X : Type) : AtMostCountable X ↔ Countable X

theorem Chapter8.CountablyInfinite.iff_image_inj {A : Type} (X : Set A) : CountablyInfinite ↑X ↔ ∃ (f : ℕ ↪ A), X = ⇑f '' Set.univ

theorem Chapter8.Nat.exists_unique_min {X : Set ℕ} (hX : X.Nonempty) : ∃! m : ℕ, m ∈ X ∧ ∀ n ∈ X, m ≤ n

Proposition 8.1.4 (Well ordering principle / Exercise 8.1.2

def Chapter8.Int.exists_unique_min : Decidable (∀ (X : Set ℤ), X.Nonempty → ∃! m : ℤ, m ∈ X ∧ ∀ n ∈ X, m ≤ n)

Equations

• Chapter8.Int.exists_unique_min = sorry

def Chapter8.NNRat.exists_unique_min : Decidable (∀ (X : Set ℚ≥0), X.Nonempty → ∃! m : ℚ≥0, m ∈ X ∧ ∀ n ∈ X, m ≤ n)

Equations

• Chapter8.NNRat.exists_unique_min = sorry

@[reducible, inline]

noncomputable abbrev Chapter8.Nat.min (X : Set ℕ) : ℕ

Equations

• Chapter8.Nat.min X = if hX : X.Nonempty then ⋯.choose else 0

theorem Chapter8.Nat.min_spec {X : Set ℕ} (hX : X.Nonempty) : min X ∈ X ∧ ∀ n ∈ X, min X ≤ n

theorem Chapter8.Nat.min_eq {X : Set ℕ} (hX : X.Nonempty) {a : ℕ} (ha : a ∈ X ∧ ∀ n ∈ X, a ≤ n) : min X = a

@[simp]

theorem Chapter8.Nat.min_empty : min ∅ = 0

theorem Chapter8.Nat.min_eq_sInf {X : Set ℕ} (hX : X.Nonempty) : min X = sInf X

theorem Chapter8.Nat.min_eq_find {X : Set ℕ} (hX : X.Nonempty) : min X = Nat.find hX

Equivalence with Mathlib's Nat.find method

theorem Chapter8.Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite ↑X] : ∃! f : ℕ → ↑X, Function.Bijective f ∧ StrictMono f

Proposition 8.1.5

theorem Chapter8.Nat.countable_of_infinite (X : Set ℕ) [Infinite ↑X] : CountablyInfinite ↑X

theorem Chapter8.Nat.atMostCountable_subset (X : Set ℕ) : AtMostCountable ↑X

Corollary 8.1.6

theorem Chapter8.AtMostCountable.subset {X : Type} (hX : AtMostCountable X) (Y : Set X) : AtMostCountable ↑Y

Corollary 8.1.7

theorem Chapter8.AtMostCountable.subset' {A : Type} {X Y : Set A} (hX : AtMostCountable ↑X) (hY : Y ⊆ X) : AtMostCountable ↑Y

theorem Chapter8.AtMostCountable.image_nat (Y : Type) (f : ℕ → Y) : AtMostCountable ↑(f '' Set.univ)

Proposition 8.1.8 / Exercise 8.1.4

theorem Chapter8.AtMostCountable.image {X : Type} (hX : CountablyInfinite X) {Y : Type} (f : X → Y) : AtMostCountable ↑(f '' Set.univ)

Corollary 8.1.9 / Exercise 8.1.5

theorem Chapter8.CountablyInfinite.union {A : Type} {X Y : Set A} (hX : CountablyInfinite ↑X) (hY : CountablyInfinite ↑Y) : CountablyInfinite ↑(X ∪ Y)

Proposition 8.1.10 / Exercise 8.1.7

theorem Chapter8.Int.countablyInfinite : CountablyInfinite ℤ

Corollary 8.1.11 -

theorem Chapter8.CountablyInfinite.lower_diag : CountablyInfinite ↑{n : ℕ × ℕ | n.2 ≤ n.1}

Lemma 8.1.12

theorem Chapter8.CountablyInfinite.prod_nat : CountablyInfinite (ℕ × ℕ)

Corollary 8.1.13

theorem Chapter8.CountablyInfinite.prod {X Y : Type} (hX : CountablyInfinite X) (hY : CountablyInfinite Y) : CountablyInfinite (X × Y)

Corollary 8.1.14 / Exercise 8.1.8

theorem Chapter8.Rat.countablyInfinite : CountablyInfinite ℚ

Corollary 8.1.15

@[reducible, inline]

abbrev Chapter8.explicit_bijection : ℕ → ℚ

Exercise 8.1.10. Note the lack of the noncomputable keyword in the abbrev.

Equations

• Chapter8.explicit_bijection = sorry

theorem Chapter8.explicit_bijection_spec : Function.Bijective explicit_bijection