Аналіз I, Розділ 8.1: Зліченість

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

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

• Власні означення для «рівної кардинальності», «зліченості» та «не більше ніж злічено». Зауважте, що тип-класи Countable у Mathlib відповідає тому, що в цьому тексті називається «не більше ніж злічена».
• Зліченість цілих чисел та раціональних чисел.

Зауважте, що оскільки теорія множин з Розділу 3 більше не використовується, ми не будемо повторно використовувати відповідні конструкції з тієї теорії тут, натомість замінюючи їх відповідниками з Mathlib.

@[reducible, inline]

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

Визначення рівної кардинальності. З міркувань простоти ми обмежуємось універсумом Type 0. Це аналогічно Chapter3.SetTheory.Set.EqualCard, але ми не використовуємо останній, оскільки теорія множин з Розділу 3 застаріла.

Equations

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

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

Взаємозв'язок з концепцією Equiv у Mathlib

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

Еквівалентність з поняттям Cardinal.mk у Mathlib

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)

Еквівалентність з поняттям Denumerable у Mathlib (див. зауваження 8.1.2)

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

Еквівалентність з типкласом Countable у Mathlib

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

Твердження 8.1.4 (Принцип цілкового впорядкування / Вправа 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

Еквівалентність з методом Nat.find у Mathlib

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

Твердження 8.1.5

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

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

Наслідок 8.1.6

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

Наслідок 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)

Твердження 8.1.8 / Вправа 8.1.4

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

Наслідок 8.1.9 / Вправа 8.1.5

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

Твердження 8.1.10 / Вправа 8.1.7

theorem Chapter8.Int.countablyInfinite : CountablyInfinite ℤ

Наслідок 8.1.11 -

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

Лема 8.1.12

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

Наслідок 8.1.13

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

Наслідок 8.1.14 / Вправа 8.1.8

theorem Chapter8.Rat.countablyInfinite : CountablyInfinite ℚ

Наслідок 8.1.15

@[reducible, inline]

abbrev Chapter8.explicit_bijection : ℕ → ℚ

Вправа 8.1.10. Зауважте відсутність ключового слова noncomputable в abbrev.

Equations

• Chapter8.explicit_bijection = sorry

theorem Chapter8.explicit_bijection_spec : Function.Bijective explicit_bijection