1. Analysis
  2. 8.1. Countability
Imports
import Mathlib.Tactic

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.

namespace Chapter8

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.

abbrev EqualCard (X Y : Type) : Prop := ∃ f : X → Y, Function.Bijective f

Relation with Mathlib's Equiv concept

theorem EqualCard.iff {X Y : Type} : EqualCard X Y ↔ Nonempty (X ≃ Y) := X:TypeY:Type⊢ EqualCard X Y ↔ Nonempty (X ≃ Y) X:TypeY:Type⊢ (∃ f, Function.Bijective f) ↔ Nonempty (X ≃ Y); X:TypeY:Type⊢ (∃ f, Function.Bijective f) → Nonempty (X ≃ Y)X:TypeY:Type⊢ Nonempty (X ≃ Y) → ∃ f, Function.Bijective f X:TypeY:Type⊢ (∃ f, Function.Bijective f) → Nonempty (X ≃ Y) X:TypeY:Typef:X → Yhf:Function.Bijective f⊢ Nonempty (X ≃ Y); All goals completed! 🐙 X:TypeY:Typee:X ≃ Y⊢ ∃ f, Function.Bijective f; All goals completed! 🐙

Equivalence with Mathlib's Cardinal.­mk concept

theorem EqualCard.iff' {X Y : Type} : EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y := X:TypeY:Type⊢ EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y All goals completed! 🐙
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 := X:TypeY:TypehXY:EqualCard X Y⊢ EqualCard Y X All goals completed! 🐙theorem declaration uses `sorry`EqualCard.trans {X Y Z : Type} (hXY : EqualCard X Y) (hYZ : EqualCard Y Z) : EqualCard X Z := X:TypeY:TypeZ:TypehXY:EqualCard X YhYZ:EqualCard Y Z⊢ EqualCard X Z All 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, X:Type⊢ Function.Surjective Subtype.val X:Typeb✝:X⊢ ∃ a, ↑a = b✝; All 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 := X:TypeY:TypehXY:EqualCard X Y⊢ Finite X ↔ Finite Y X:TypeY:Typef:X → Yhf:Function.Bijective f⊢ Finite X ↔ Finite Y; All goals completed! 🐙theorem AtMostCountable.equiv {X Y: Type} (hXY : EqualCard X Y) : AtMostCountable X ↔ AtMostCountable Y := X:TypeY:TypehXY:EqualCard X Y⊢ AtMostCountable X ↔ AtMostCountable Y All goals completed! 🐙

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

theorem CountablyInfinite.iff (X : Type) : CountablyInfinite X ↔ Nonempty (Denumerable X) := X:Type⊢ CountablyInfinite X ↔ Nonempty (Denumerable X) X:Type⊢ Nonempty (X ≃ ℕ) ↔ Nonempty (Denumerable X); X:Type⊢ Nonempty (X ≃ ℕ) → Nonempty (Denumerable X)X:Type⊢ Nonempty (Denumerable X) → Nonempty (X ≃ ℕ) X:Type⊢ Nonempty (X ≃ ℕ) → Nonempty (Denumerable X) X:Typee:X ≃ ℕ⊢ Nonempty (Denumerable X); All goals completed! 🐙 X:Typeh:Denumerable X⊢ Nonempty (X ≃ ℕ); All goals completed! 🐙

Equivalence with Mathlib's Countable typeclass

theorem CountablyInfinite.iff' (X : Type) : CountablyInfinite X ↔ Countable X ∧ Infinite X := X:Type⊢ CountablyInfinite X ↔ Countable X ∧ Infinite X All goals completed! 🐙
theorem CountablyInfinite.toCountable {X : Type} (hX: CountablyInfinite X) : Countable X := X:TypehX:CountablyInfinite X⊢ Countable X All goals completed! 🐙theorem CountablyInfinite.toInfinite {X : Type} (hX: CountablyInfinite X) : Infinite X := X:TypehX:CountablyInfinite X⊢ Infinite X All goals completed! 🐙theorem AtMostCountable.iff (X : Type) : AtMostCountable X ↔ Countable X := X:Type⊢ AtMostCountable X ↔ Countable X X:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite X⊢ AtMostCountable X ↔ Countable X X:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite Xh2:Finite X ∨ Infinite X⊢ AtMostCountable X ↔ Countable X X:Typeh1:CountablyInfinite X ↔ Countable X ∧ Infinite Xh2:Finite X ∨ Infinite Xh3:Finite X → Countable X⊢ AtMostCountable X ↔ Countable X All goals completed! 🐙theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite X ↔ ∃ f : ℕ ↪ A, X = f '' .univ := A:TypeX:Set A⊢ CountablyInfinite ↑X ↔ ∃ f, X = ⇑f '' Set.univ A:TypeX:Set A⊢ CountablyInfinite ↑X → ∃ f, X = ⇑f '' Set.univA:TypeX:Set A⊢ (∃ f, X = ⇑f '' Set.univ) → CountablyInfinite ↑X A:TypeX:Set A⊢ CountablyInfinite ↑X → ∃ f, X = ⇑f '' Set.univ A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective g⊢ ∃ f, X = ⇑f '' Set.univ A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ ∃ f, X = ⇑f '' Set.univ A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ Function.Injective (Subtype.val ∘ f)A: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 A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f g⊢ Function.Injective (Subtype.val ∘ f) intro x A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx:ℕy:ℕ⊢ (Subtype.val ∘ f) x = (Subtype.val ∘ f) y → x = y A: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; A: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; All goals completed! 🐙 A: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; A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X ↔ ∃ y, ↑(f y) = x✝; A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X → ∃ y, ↑(f y) = x✝A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ (∃ y, ↑(f y) = x✝) → x✝ ∈ X A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:A⊢ x✝ ∈ X → ∃ y, ↑(f y) = x✝ A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gx✝:Ahx:x✝ ∈ X⊢ ∃ y, ↑(f y) = x✝; A: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✝; All goals completed! 🐙 A:TypeX:Set Ag:↑X → ℕhg:Function.Bijective gf:ℕ → ↑Xhleft:Function.LeftInverse f ghright:Function.RightInverse f gw✝:ℕ⊢ ↑(f w✝) ∈ X; All goals completed! 🐙 A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univ⊢ CountablyInfinite ↑X A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑f⊢ CountablyInfinite ↑X A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑f⊢ Function.Bijective (Function.invFun ⇑f ∘ Subtype.val); A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑f⊢ Function.Injective (Function.invFun ⇑f ∘ Subtype.val)A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑f⊢ Function.Surjective (Function.invFun ⇑f ∘ Subtype.val) A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑f⊢ Function.Injective (Function.invFun ⇑f ∘ Subtype.val) A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑fx:Ahx:x ∈ Xy:Ahy:y ∈ Xh:(Function.invFun ⇑f ∘ Subtype.val) ⟨x, hx⟩ = (Function.invFun ⇑f ∘ Subtype.val) ⟨y, hy⟩⊢ ⟨x, hx⟩ = ⟨y, hy⟩; All goals completed! 🐙 A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑fn:ℕ⊢ ∃ a, (Function.invFun ⇑f ∘ Subtype.val) a = n; use ⟨ f n, A:TypeX:Set Af:ℕ ↪ Ahf:X = ⇑f '' Set.univthis:Function.LeftInverse (Function.invFun ⇑f) ⇑fn:ℕ⊢ f n ∈ X All goals completed! 🐙 ⟩; All goals completed! 🐙/-- Examples 8.1.3 -/ declaration uses `sorry`example : CountablyInfinite ℕ := ⊢ CountablyInfinite ℕ All goals completed! 🐙declaration uses `sorry`example : CountablyInfinite (.univ \ {0}: Set ℕ) := ⊢ CountablyInfinite ↑(Set.univ \ {0}) All goals completed! 🐙declaration uses `sorry`example : CountablyInfinite ((fun n:ℕ ↦ 2*n) '' .univ) := ⊢ CountablyInfinite ↑((fun n ↦ 2 * n) '' Set.univ) All goals completed! 🐙

Proposition 8.1.4 (Well ordering principle / Exercise 8.1.2

theorem declaration uses `sorry`Nat.exists_unique_min {X : Set ℕ} (hX : X.Nonempty) : ∃! m ∈ X, ∀ n ∈ X, m ≤ n := X:Set ℕhX:X.Nonempty⊢ ∃! m, m ∈ X ∧ ∀ n ∈ X, m ≤ n All goals completed! 🐙
def declaration uses `sorry`Int.exists_unique_min : Decidable (∀ (X : Set ℤ) (hX : X.Nonempty), ∃! m ∈ X, ∀ n ∈ X, m ≤ n) := ⊢ 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`. All goals completed! 🐙def declaration uses `sorry`NNRat.exists_unique_min : Decidable (∀ (X : Set NNRat) (hX : X.Nonempty), ∃! m ∈ X, ∀ n ∈ X, m ≤ n) := ⊢ 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`. All 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 := X:Set ℕhX:X.Nonempty⊢ min X ∈ X ∧ ∀ n ∈ X, min X ≤ n X:Set ℕhX:X.Nonempty⊢ ⋯.choose ∈ X ∧ ∀ n ∈ X, ⋯.choose ≤ n; All 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 := ⊢ min ∅ = 0 All goals completed! 🐙declaration uses `sorry`example : Nat.min ((fun n ↦ 2*n) '' (.Ici 1)) = 2 := ⊢ Nat.min ((fun n ↦ 2 * n) '' Set.Ici 1) = 2 All goals completed! 🐙theorem declaration uses `sorry`Nat.min_eq_sInf {X : Set ℕ} (hX : X.Nonempty) : min X = sInf X := X:Set ℕhX:X.Nonempty⊢ min X = sInf X All goals completed! 🐙

Equivalence with Mathlib's Nat.­find method

open Classical intheorem Nat.min_eq_find {X : Set ℕ} (hX : X.Nonempty) : min X = Nat.find hX := X:Set ℕhX:X.Nonempty⊢ min X = Nat.find hX X:Set ℕhX:X.Nonempty⊢ Nat.find hX = min X; X:Set ℕhX:X.Nonempty⊢ min X ∈ X ∧ ∀ n < min X, n ∉ X; X:Set ℕhX:X.Nonemptythis:min X ∈ X ∧ ∀ n ∈ X, min X ≤ n⊢ min X ∈ X ∧ ∀ n < min X, n ∉ X; All goals completed! 🐙

Proposition 8.1.5

theorem declaration uses `sorry`Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite X] : ∃! f : ℕ → X, Function.Bijective f ∧ StrictMono f := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f -- This proof is written to follow the structure of the original text. X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) t⊢ ∃! f, Function.Bijective f ∧ StrictMono f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}⊢ ∃! f, Function.Bijective f ∧ StrictMono f have ha_infinite (n:ℕ) : Infinite { x ∈ X | ∀ (m:ℕ) (h:m < n), x ≠ a m } := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonempty⊢ ∃! f, Function.Bijective f ∧ StrictMono f have ha_mono : StrictMono a := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 have ha_injective : Function.Injective a := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 have haX (n:ℕ) : a n ∈ X := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩⊢ ∃! f, Function.Bijective f ∧ StrictMono f have hf_injective : Function.Injective f := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f intro x X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩x:ℕy:ℕ⊢ f x = f y → x = y X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩x:ℕy:ℕhxy:f x = f y⊢ x = y; X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩x:ℕy:ℕhxy:a x = a y⊢ x = y; All goals completed! 🐙 have hf_surjective : Function.Surjective f := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fx:ℕhx:x ∈ X⊢ ∃ a, f a = ⟨x, hx⟩; X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fx:ℕhx:x ∈ X⊢ ∃ a_1, a a_1 = x; X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fx:ℕhx:x ∈ Xthis:¬∃ a_1, a a_1 = x⊢ False have h1 (n:ℕ) : x ∈ { x ∈ X | ∀ (m:ℕ) (h:m < n), x ≠ a m } := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 have h2 (n:ℕ) : x ≥ a n := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fx:ℕhx:x ∈ Xthis:¬∃ a_1, a a_1 = xh1:∀ (n : ℕ), x ∈ {x | x ∈ X ∧ ∀ m < n, x ≠ a m}n:ℕ⊢ x ≥ min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}; All goals completed! 🐙 have h3 (n:ℕ) : a n ≥ n := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fx:ℕhx:x ∈ Xthis:¬∃ a_1, a a_1 = xh1:∀ (n : ℕ), x ∈ {x | x ∈ X ∧ ∀ m < n, x ≠ a m}h2:∀ (n : ℕ), x ≥ a nh3:∀ (n : ℕ), a n ≥ nh4:∀ (n : ℕ), x ≥ n⊢ False All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective f⊢ ∀ (y : ℕ → ↑X), Function.Bijective y ∧ StrictMono y → y = f intro g X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono g⊢ g = f; X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:g ≠ f⊢ False replace : { n | g n ≠ f n }.Nonempty := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n} = ∅⊢ g = f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n} = ∅⊢ ∀ (x : ℕ), g x = f x; All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}⊢ False X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}hm:g m ≠ f m⊢ False have hm' {n:ℕ} (hn: n < m) : g n = f n := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}hm:g m ≠ f mn:ℕhn:n < mhgfn:¬g n = f n⊢ False; linarith [(min_spec this).2 n (X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}hm:g m ≠ f mn:ℕhn:n < mhgfn:¬g n = f n⊢ n ∈ {n | g n ≠ f n} All goals completed! 🐙)] have hgm : g m = min { x ∈ X | ∀ (n:ℕ) (h:n < m), x ≠ a n } := X:Set ℕinst✝:Infinite ↑X⊢ ∃! f, Function.Bijective f ∧ StrictMono f All goals completed! 🐙 X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}hm:g m ≠ f mhm':∀ {n : ℕ}, n < m → g n = f nhgm:↑(g m) = a m⊢ False; X:Set ℕinst✝:Infinite ↑Xa:ℕ → ℕ := fun t ↦ Nat.strongRec (fun n a ↦ min {x | x ∈ X ∧ ∀ (m : ℕ) (h : m < n), x ≠ a m h}) tha:∀ (n : ℕ), a n = min {x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_infinite:∀ (n : ℕ), Infinite ↑{x | x ∈ X ∧ ∀ m < n, x ≠ a m}ha_nonempty:∀ (n : ℕ), {x | x ∈ X ∧ ∀ m < n, x ≠ a m}.Nonemptyha_mono:StrictMono aha_injective:Function.Injective ahaX:∀ (n : ℕ), a n ∈ Xf:ℕ → ↑X := fun n ↦ ⟨a n, ⋯⟩hf_injective:Function.Injective fhf_surjective:Function.Surjective fg:ℕ → ↑Xhg_bijective:Function.Bijective ghg_mono:StrictMono gthis:{n | g n ≠ f n}.Nonemptym:ℕ := min {n | g n ≠ f n}hm':∀ {n : ℕ}, n < m → g n = f nhgm:↑(g m) = a mhm:True⊢ g m = f m; All goals completed! 🐙
theorem Nat.countable_of_infinite (X : Set ℕ) [Infinite X] : CountablyInfinite X := X:Set ℕinst✝:Infinite ↑X⊢ CountablyInfinite ↑X X:Set ℕinst✝:Infinite ↑Xthis:∃ x, Function.Bijective x ∧ StrictMono x⊢ CountablyInfinite ↑X All goals completed! 🐙

Corollary 8.1.6

theorem Nat.atMostCountable_subset (X: Set ℕ) : AtMostCountable X := X:Set ℕ⊢ AtMostCountable ↑X X:Set ℕh✝:Finite ↑X⊢ AtMostCountable ↑XX:Set ℕh✝:Infinite ↑X⊢ AtMostCountable ↑X X:Set ℕh✝:Finite ↑X⊢ AtMostCountable ↑X All goals completed! 🐙 All goals completed! 🐙

Corollary 8.1.7

theorem declaration uses `sorry`AtMostCountable.subset {X: Type} (hX : AtMostCountable X) (Y: Set X) : AtMostCountable Y := X:TypehX:AtMostCountable XY:Set X⊢ AtMostCountable ↑Y -- This proof is written to follow the structure of the original text. X:TypeY:Set Xf:X → ℕhf:Function.Bijective f⊢ AtMostCountable ↑YX:TypeY:Set XhX:Finite X⊢ AtMostCountable ↑Y X:TypeY:Set Xf:X → ℕhf:Function.Bijective f⊢ AtMostCountable ↑Y let f' : Y → f '' Y := fun y ↦ ⟨ f y, X:TypeY:Set Xf:X → ℕhf:Function.Bijective fy:↑Y⊢ f ↑y ∈ f '' Y All goals completed! 🐙 ⟩ have hf' : Function.Bijective f' := X:TypehX:AtMostCountable XY:Set X⊢ AtMostCountable ↑Y All goals completed! 🐙 X:TypeY:Set Xf:X → ℕhf:Function.Bijective ff':↑Y → ↑(f '' Y) := fun y ↦ ⟨f ↑y, ⋯⟩hf':Function.Bijective f'⊢ AtMostCountable ↑(f '' Y); All goals completed! 🐙 All goals completed! 🐙
theorem AtMostCountable.subset' {A: Type} {X Y: Set A} (hX: AtMostCountable X) (hY: Y ⊆ X) : AtMostCountable Y := A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ AtMostCountable ↑Y A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Injective fun y ↦ ⟨↑↑y, ⋯⟩A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Surjective fun y ↦ ⟨↑↑y, ⋯⟩ A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ X⊢ Function.Injective fun y ↦ ⟨↑↑y, ⋯⟩ intro ⟨ ⟨ _, _ ⟩, _ ⟩ A: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}⊢ (fun y ↦ ⟨↑↑y, ⋯⟩) ⟨⟨val✝¹, property✝³⟩, property✝²⟩ = (fun y ↦ ⟨↑↑y, ⋯⟩) ⟨⟨val✝, property✝¹⟩, property✝⟩ → ⟨⟨val✝¹, property✝³⟩, property✝²⟩ = ⟨⟨val✝, property✝¹⟩, property✝⟩ A: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✝⟩; All goals completed! 🐙 A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ Xy:Ahy:y ∈ Y⊢ ∃ a, (fun y ↦ ⟨↑↑y, ⋯⟩) a = ⟨y, hy⟩; use ⟨ ⟨ y, hY hy ⟩, A:TypeX:Set AY:Set AhX:AtMostCountable ↑XhY:Y ⊆ Xy:Ahy:y ∈ Y⊢ ⟨y, ⋯⟩ ∈ {x | ↑x ∈ Y} All goals completed! 🐙 ⟩

Proposition 8.1.8 / Exercise 8.1.4

theorem declaration uses `sorry`AtMostCountable.image_nat (Y: Type) (f: ℕ → Y) : AtMostCountable (f '' .univ) := Y:Typef:ℕ → Y⊢ AtMostCountable ↑(f '' Set.univ) All goals completed! 🐙

Corollary 8.1.9 / Exercise 8.1.5

theorem declaration uses `sorry`AtMostCountable.image {X:Type} (hX: CountablyInfinite X) {Y: Type} (f: X → Y) : AtMostCountable (f '' .univ) := X:TypehX:CountablyInfinite XY:Typef:X → Y⊢ AtMostCountable ↑(f '' Set.univ) All goals completed! 🐙

Proposition 8.1.10 / Exercise 8.1.7

theorem declaration uses `sorry`CountablyInfinite.union {A:Type} {X Y: Set A} (hX: CountablyInfinite X) (hY: CountablyInfinite Y) : CountablyInfinite (X ∪ Y: Set A) := A:TypeX:Set AY:Set AhX:CountablyInfinite ↑XhY:CountablyInfinite ↑Y⊢ CountablyInfinite ↑(X ∪ Y) All goals completed! 🐙

Corollary 8.1.11 -

theorem Int.countablyInfinite : CountablyInfinite ℤ := ⊢ CountablyInfinite ℤ -- This proof is written to follow the structure of the original text. have h1 : CountablyInfinite {n:ℤ | n ≥ 0} := ⊢ CountablyInfinite ℤ ⊢ ∃ f, {n | n ≥ 0} = ⇑f '' Set.univ use ⟨ (↑·:ℕ → ℤ), ⊢ Function.Injective fun x ↦ ↑x intro _ a₁✝:ℕa₂✝:ℕ⊢ (fun x ↦ ↑x) a₁✝ = (fun x ↦ ↑x) a₂✝ → a₁✝ = a₂✝ a₁✝:ℕa₂✝:ℕa✝:(fun x ↦ ↑x) a₁✝ = (fun x ↦ ↑x) a₂✝⊢ a₁✝ = a₂✝; All goals completed! 🐙 ⟩ n:ℤ⊢ n ∈ {n | n ≥ 0} ↔ n ∈ ⇑{ toFun := fun x ↦ ↑x, inj' := ⋯ } '' Set.univ; n:ℤ⊢ 0 ≤ n ↔ ∃ y, ↑y = n; refine ⟨ ?_, n:ℤ⊢ (∃ y, ↑y = n) → 0 ≤ n All goals completed! 🐙 ⟩ n:ℤ⊢ 0 ≤ n → ∃ y, ↑y = n n:ℤh:0 ≤ n⊢ ∃ y, ↑y = n; n:ℤh:0 ≤ n⊢ ↑n.toNat = n; All goals completed! 🐙 have h2 : CountablyInfinite {n:ℤ | n ≤ 0} := ⊢ CountablyInfinite ℤ h1:CountablyInfinite ↑{n | n ≥ 0}⊢ ∃ f, {n | n ≤ 0} = ⇑f '' Set.univ use ⟨ (-↑·:ℕ → ℤ), h1:CountablyInfinite ↑{n | n ≥ 0}⊢ Function.Injective fun x ↦ -↑x intro _ h1:CountablyInfinite ↑{n | n ≥ 0}a₁✝:ℕa₂✝:ℕ⊢ (fun x ↦ -↑x) a₁✝ = (fun x ↦ -↑x) a₂✝ → a₁✝ = a₂✝ h1:CountablyInfinite ↑{n | n ≥ 0}a₁✝:ℕa₂✝:ℕa✝:(fun x ↦ -↑x) a₁✝ = (fun x ↦ -↑x) a₂✝⊢ a₁✝ = a₂✝; All goals completed! 🐙 ⟩ h1:CountablyInfinite ↑{n | n ≥ 0}n:ℤ⊢ n ∈ {n | n ≤ 0} ↔ n ∈ ⇑{ toFun := fun x ↦ -↑x, inj' := ⋯ } '' Set.univ; h1:CountablyInfinite ↑{n | n ≥ 0}n:ℤ⊢ n ≤ 0 ↔ ∃ y, -↑y = n; refine ⟨ ?_, h1:CountablyInfinite ↑{n | n ≥ 0}n:ℤ⊢ (∃ y, -↑y = n) → n ≤ 0 All goals completed! 🐙 ⟩ h1:CountablyInfinite ↑{n | n ≥ 0}n:ℤh:n ≤ 0⊢ ∃ y, -↑y = n; h1:CountablyInfinite ↑{n | n ≥ 0}n:ℤh:n ≤ 0⊢ -↑(-n).toNat = n; All goals completed! 🐙 have : CountablyInfinite (.univ : Set ℤ) := ⊢ CountablyInfinite ℤ h1:CountablyInfinite ↑{n | n ≥ 0}h2:CountablyInfinite ↑{n | n ≤ 0}⊢ Set.univ = {n | n ≥ 0} ∪ {n | n ≤ 0}; h1:CountablyInfinite ↑{n | n ≥ 0}h2:CountablyInfinite ↑{n | n ≤ 0}x✝:ℤ⊢ x✝ ∈ Set.univ ↔ x✝ ∈ {n | n ≥ 0} ∪ {n | n ≤ 0}; h1:CountablyInfinite ↑{n | n ≥ 0}h2:CountablyInfinite ↑{n | n ≤ 0}x✝:ℤ⊢ 0 ≤ x✝ ∨ x✝ ≤ 0; All goals completed! 🐙 rwa [←CountablyInfinite.equiv (.univ _)h1:CountablyInfinite ↑{n | n ≥ 0}h2:CountablyInfinite ↑{n | n ≤ 0}this:CountablyInfinite ↑Set.univ⊢ CountablyInfinite ↑Set.univ

Lemma 8.1.12

theorem declaration uses `sorry`CountablyInfinite.lower_diag : CountablyInfinite { n : ℕ × ℕ | n.2 ≤ n.1 } := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} -- This proof is written to follow the structure of the original text. A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), m⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} have ha : StrictMono a := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} All goals completed! 🐙 A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + m⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} have hf : Function.Injective f := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:(n, m) ∈ An':ℕm':ℕhnm':(n', m') ∈ Ah:f ⟨(n, m), hnm⟩ = f ⟨(n', m'), hnm'⟩⊢ ⟨(n, m), hnm⟩ = ⟨(n', m'), hnm'⟩ A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'⊢ n = n' ∧ m = m' A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n < n'⊢ n = n' ∧ m = m'A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nm':ℕhnm':m' ≤ nh:a n + m = a n + m'⊢ n = n ∧ m = m'A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n' < n⊢ n = n' ∧ m = m' A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n < n'⊢ n = n' ∧ m = m' have : a n' + m' > a n + m := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} calc _ ≥ a n' := A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n < n'⊢ a n' + m' ≥ a n' All goals completed! 🐙 _ ≥ a (n+1) := ha.monotone (A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n < n'⊢ n + 1 ≤ n' All goals completed! 🐙) _ = a n + (n + 1) := Finset.sum_range_succ id _ _ > a n + m := A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n < n'⊢ a n + (n + 1) > a n + m All goals completed! 🐙 All goals completed! 🐙 A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nm':ℕhnm':m' ≤ nh:a n + m = a n + m'⊢ n = n ∧ m = m' All goals completed! 🐙 have : a n + m > a n' + m' := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} calc _ ≥ a n := A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n' < n⊢ a n + m ≥ a n All goals completed! 🐙 _ ≥ a (n'+1) := ha.monotone (A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n' < n⊢ n' + 1 ≤ n All goals completed! 🐙) _ = a n' + (n' + 1) := Finset.sum_range_succ id _ _ > a n' + m' := A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mn:ℕm:ℕhnm:m ≤ nn':ℕm':ℕhnm':m' ≤ n'h:a n + m = a n' + m'hnn':n' < n⊢ a n' + (n' + 1) > a n' + m' All goals completed! 🐙 All goals completed! 🐙 let f' : A → f '' .univ := fun p ↦ ⟨ f p, A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective fp:↑A⊢ f p ∈ f '' Set.univ All goals completed! 🐙 ⟩ have hf' : Function.Bijective f' := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩⊢ Function.Injective f'A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩⊢ Function.Surjective f' A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩⊢ Function.Injective f' intro p A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩p:↑Aq:↑A⊢ f' p = f' q → p = q A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩p:↑Aq:↑Ahpq:f' p = f' q⊢ p = q; A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩p:↑Aq:↑Ahpq:f p = f q⊢ p = q; All goals completed! 🐙 A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩l:ℕhl:l ∈ f '' Set.univ⊢ ∃ a, f' a = ⟨l, hl⟩; A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩l:ℕhl✝:l ∈ f '' Set.univhl:∃ a b, ∃ (b_1 : (a, b) ∈ A), f ⟨(a, b), b_1⟩ = l⊢ ∃ a, f' a = ⟨l, hl⟩ A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩n:ℕm:ℕq:(n, m) ∈ Ahl:f ⟨(n, m), q⟩ ∈ f '' Set.univ⊢ ∃ a, f' a = ⟨f ⟨(n, m), q⟩, hl⟩; All goals completed! 🐙 have : AtMostCountable A := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩hf':Function.Bijective f'⊢ AtMostCountable ↑(f '' Set.univ); All goals completed! 🐙 have hfin : ¬ Finite A := ⊢ CountablyInfinite ↑{n | n.2 ≤ n.1} All goals completed! 🐙 A:Set (ℕ × ℕ) := {n | n.2 ≤ n.1}a:ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n + 1), mha:StrictMono af:↑A → ℕ := fun x ↦ match x with | ⟨(n, m), property⟩ => a n + mhf:Function.Injective ff':↑A → ↑(f '' Set.univ) := fun p ↦ ⟨f p, ⋯⟩hf':Function.Bijective f'this:CountablyInfinite ↑A ∨ Finite ↑Ahfin:¬Finite ↑A⊢ CountablyInfinite ↑{n | n.2 ≤ n.1}; All goals completed! 🐙

Corollary 8.1.13

theorem CountablyInfinite.prod_nat : CountablyInfinite (ℕ × ℕ) := ⊢ CountablyInfinite (ℕ × ℕ) have upper_diag : CountablyInfinite { n : ℕ × ℕ | n.1 ≤ n.2 } := ⊢ CountablyInfinite (ℕ × ℕ) refine (equiv ⟨ fun ⟨ (n, m), _ ⟩ ↦ ⟨ (m, n), x✝:↑{n | n.2 ≤ n.1}n:ℕm:ℕproperty✝:(n, m) ∈ {n | n.2 ≤ n.1}⊢ (m, n) ∈ {n | n.1 ≤ n.2} All goals completed! 🐙 ⟩, ?_, ?_ ⟩).mp lower_diag ⊢ Function.Injective fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩ intro ⟨ (_, _), _ ⟩ fst✝¹:ℕsnd✝¹:ℕproperty✝¹:(fst✝¹, snd✝¹) ∈ {n | n.2 ≤ n.1}fst✝:ℕsnd✝:ℕproperty✝:(fst✝, snd✝) ∈ {n | n.2 ≤ n.1}⊢ (fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩) ⟨(fst✝¹, snd✝¹), property✝¹⟩ = (fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩) ⟨(fst✝, snd✝), property✝⟩ → ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩ fst✝¹:ℕsnd✝¹:ℕproperty✝¹:(fst✝¹, snd✝¹) ∈ {n | n.2 ≤ n.1}fst✝:ℕsnd✝:ℕproperty✝:(fst✝, snd✝) ∈ {n | n.2 ≤ n.1}a✝:(fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩) ⟨(fst✝¹, snd✝¹), property✝¹⟩ = (fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩) ⟨(fst✝, snd✝), property✝⟩⊢ ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩; All goals completed! 🐙 n:ℕm:ℕproperty✝:(n, m) ∈ {n | n.1 ≤ n.2}⊢ ∃ a, (fun x ↦ match x with | ⟨(n, m), property⟩ => ⟨(m, n), ⋯⟩) a = ⟨(n, m), property✝⟩; use ⟨ (m, n), n:ℕm:ℕproperty✝:(n, m) ∈ {n | n.1 ≤ n.2}⊢ (m, n) ∈ {n | n.2 ≤ n.1} All goals completed! 🐙 ⟩ have : CountablyInfinite (.univ : Set (ℕ × ℕ)) := ⊢ CountablyInfinite (ℕ × ℕ) upper_diag:CountablyInfinite ↑{n | n.1 ≤ n.2}⊢ Set.univ = {n | n.2 ≤ n.1} ∪ {n | n.1 ≤ n.2}; upper_diag:CountablyInfinite ↑{n | n.1 ≤ n.2}n:ℕm:ℕ⊢ (n, m) ∈ Set.univ ↔ (n, m) ∈ {n | n.2 ≤ n.1} ∪ {n | n.1 ≤ n.2}; upper_diag:CountablyInfinite ↑{n | n.1 ≤ n.2}n:ℕm:ℕ⊢ m ≤ n ∨ n ≤ m; All goals completed! 🐙 All goals completed! 🐙

Corollary 8.1.14 / Exercise 8.1.8

theorem declaration uses `sorry`CountablyInfinite.prod {X Y:Type} (hX: CountablyInfinite X) (hY: CountablyInfinite Y) : CountablyInfinite (X × Y) := X:TypeY:TypehX:CountablyInfinite XhY:CountablyInfinite Y⊢ CountablyInfinite (X × Y) All goals completed! 🐙

Corollary 8.1.15

theorem declaration uses `sorry`Rat.countablyInfinite : CountablyInfinite ℚ := ⊢ CountablyInfinite ℚ -- This proof is written to follow the structure of the original text. have : CountablyInfinite { n:ℤ | n ≠ 0 } := ⊢ CountablyInfinite ℚ All goals completed! 🐙 this:CountablyInfinite (ℤ × ↑{n | n ≠ 0})⊢ CountablyInfinite ℚ this:CountablyInfinite (ℤ × ↑{n | n ≠ 0})f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑b⊢ CountablyInfinite ℚ f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bthis:AtMostCountable ↑(f '' Set.univ)⊢ CountablyInfinite ℚ have h : f '' .univ = .univ := ⊢ CountablyInfinite ℚ All goals completed! 🐙 f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh1:CountablyInfinite ↑(f '' Set.univ)⊢ CountablyInfinite ℚf:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh2:Finite ↑(f '' Set.univ)⊢ CountablyInfinite ℚ f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh1:CountablyInfinite ↑(f '' Set.univ)⊢ CountablyInfinite ℚ f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh1:CountablyInfinite ↑(f '' Set.univ)h1':CountablyInfinite ↑Set.univ⊢ CountablyInfinite ℚ rwa [CountablyInfinite.equiv (EqualCard.univ _)f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh1:CountablyInfinite ↑(f '' Set.univ)h1':CountablyInfinite ℚ⊢ CountablyInfinite ℚ at h1' f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh2:Finite ↑(f '' Set.univ)⊢ CountablyInfinite ℚ f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh2:Finite ↑(f '' Set.univ)h2':Finite ↑Set.univ⊢ CountablyInfinite ℚ f:ℤ × ↑{n | n ≠ 0} → ℚ := fun x ↦ match x with | (a, b) => ↑a / ↑↑bh:f '' Set.univ = Set.univh2:Finite ↑(f '' Set.univ)h2':Finite ℚ⊢ CountablyInfinite ℚ All goals completed! 🐙
/-- Exercise 8.1.1 -/ declaration uses `sorry`example (X: Type) : Infinite X ↔ ∃ Y : Set X, Y ≠ .univ ∧ EqualCard Y X := X:Type⊢ Infinite X ↔ ∃ Y, Y ≠ Set.univ ∧ EqualCard (↑Y) X All goals completed! 🐙/-- Exercise 8.1.6 -/ declaration uses `sorry`example (A: Type) : AtMostCountable A ↔ ∃ f : A → ℕ, Function.Injective f := A:Type⊢ AtMostCountable A ↔ ∃ f, Function.Injective f All goals completed! 🐙/-- Exercise 8.1.9 -/ declaration uses `sorry`example {I X:Type} (hI: AtMostCountable I) (A: I → Set X) (hA: ∀ i, AtMostCountable (A i)) : AtMostCountable (⋃ i, A i) := I:TypeX:TypehI:AtMostCountable IA:I → Set XhA:∀ (i : I), AtMostCountable ↑(A i)⊢ AtMostCountable ↑(⋃ i, A i) All goals completed! 🐙

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

abbrev declaration uses `sorry`explicit_bijection : ℕ → ℚ := sorry
theorem declaration uses `sorry`explicit_bijection_spec : Function.Bijective explicit_bijection := ⊢ Function.Bijective explicit_bijection All goals completed! 🐙end Chapter8