/-- The bijection `n ↦ 2n` between `ℕ` and the even numbers, with inverse `m ↦ m / 2`. -/def doubling : ℕ ≃ {m : ℕ // Even m} where toFun n := ⟨2 * n, even_two_mul n⟩ invFun m := m.1 / 2 left_inv n := by simp right_inv m := by obtain ⟨m, k, hk⟩ := m apply Subtype.ext simp only omega
zigzag_bijectivetheoremProved here from basic factspropext, Quot.sound
zigzag_bijectiveLean 4Proved here from basic factsFormally verified
/-- **ℤ is countable**: the zigzag is a bijection `ℕ → ℤ`.*Injective:* even inputs give values `≥ 0`, odd inputs give values `< 0`, and on each kind theformula is one-to-one. *Surjective:* `z ≥ 0` is hit by `2z`, and `z < 0` by `−2z − 1`. -/theorem zigzag_bijective : Bijective zigzag := by constructor · intro a b h unfold zigzag at h split_ifs at h <;> omega · intro z rcases le_or_gt 0 z with hz | hz · refine ⟨2 * z.toNat, ?_⟩ unfold zigzag split_ifs <;> omega · refine ⟨(-2 * z - 1).toNat, ?_⟩ unfold zigzag split_ifs <;> omega
rat_countabletheoremApplies a library theorempropext, Classical.choice, Quot.sound
rat_countableLean 4Applies a library theoremFormally verified
/-- **ℚ is countable**: Mathlib's instance, which encodes a fraction in lowest terms by itsnumerator and denominator (`Rat.instDenumerable`). -/theorem rat_countable : Countable ℚ := inferInstance
/-- The triangular number `tri d = 0 + 1 + ⋯ + d = d(d + 1)/2`: the number of points on thediagonals `0, 1, …, d − 1` of the grid `ℕ × ℕ` (diagonal `j` has `j + 1` points). -/def tri (d : ℕ) : ℕ := ∑ i ∈ range (d + 1), i
/-- **Cantor's pairing function** `π(m, n) = tri (m + n) + n`: walk the grid diagonal bydiagonal; the point `(m, n)` lies on diagonal `m + n`, and is the `n`-th point along it. -/def cantorPair (m n : ℕ) : ℕ := tri (m + n) + n
tri_monotheoremProved here from basic factspropext, Classical.choice, Quot.sound
tri_monoLean 4Proved here from basic factsFormally verified
/-- Triangular numbers increase: `tri a ≤ tri (a + k)`. -/theorem tri_mono (a k : ℕ) : tri a ≤ tri (a + k) := by induction k with | zero => exact le_refl _ | succ k ih => rw [← Nat.add_assoc, tri_succ]; omega
cantorPair_injectivetheoremProved here from basic factspropext, Classical.choice, Quot.sound
cantorPair_injectiveLean 4Proved here from basic factsFormally verified
/-- **Cantor's pairing is injective.** The values on diagonal `d` are `tri d, …, tri d + d`, allless than `tri (d + 1)`, where the next diagonal starts. So equal values force equal diagonals`m + n = m' + n'`, then equal positions `n = n'`, then `m = m'`. -/theorem cantorPair_injective {m n m' n' : ℕ} (h : cantorPair m n = cantorPair m' n') : m = m' ∧ n = n' := by unfold cantorPair at h have key : ∀ {d d' n : ℕ}, d < d' → n ≤ d → tri d + n < tri d' := by intro d d' n hlt hn obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hlt have h1 := tri_mono (d + 1) k rw [Nat.add_right_comm] at h1 have h2 := tri_succ d omega rcases lt_trichotomy (m + n) (m' + n') with hlt | heq | hgt · exact absurd h (Nat.ne_of_lt (lt_of_lt_of_le (key hlt (by omega)) (by omega))) · rw [heq] at h omega · exact absurd h (Nat.ne_of_gt (lt_of_lt_of_le (key hgt (by omega)) (by omega)))
cantorPair_surjectivetheoremProved here from basic factspropext, Classical.choice, Quot.sound
cantorPair_surjectiveLean 4Proved here from basic factsFormally verified
/-- **Cantor's pairing is surjective**, by induction on the value `k`: if `π(m, n) = k`, the nextvalue `k + 1` is the next point of the walk — one step up the same diagonal, `(m − 1, n + 1)`, or,at the end of a diagonal (`m = 0`), the first point `(n + 1, 0)` of the next one. -/theorem cantorPair_surjective (k : ℕ) : ∃ m n, cantorPair m n = k := by induction k with | zero => exact ⟨0, 0, rfl⟩ | succ k ih => obtain ⟨m, n, h⟩ := ih unfold cantorPair at h cases m with | zero => refine ⟨n + 1, 0, ?_⟩ unfold cantorPair rw [Nat.add_zero, tri_succ] rw [Nat.zero_add] at h omega | succ m => refine ⟨m, n + 1, ?_⟩ unfold cantorPair rw [show m + (n + 1) = m + 1 + n by omega] omega
nat_prod_equivtheoremProved here from basic factspropext, Classical.choice, Quot.sound
nat_prod_equivLean 4Proved here from basic factsFormally verified
/-- Hence **`ℕ × ℕ` has the same cardinality as `ℕ`**: Cantor's pairing is a bijection.(Mathlib has a different pairing function with the same property, `Nat.pairEquiv`.) -/theorem nat_prod_equiv : Nonempty (ℕ × ℕ ≃ ℕ) := by refine ⟨Equiv.ofBijective (fun p => cantorPair p.1 p.2) ⟨?_, ?_⟩⟩ · intro p q h obtain ⟨h1, h2⟩ := cantorPair_injective h exact Prod.ext h1 h2 · intro k obtain ⟨m, n, h⟩ := cantorPair_surjective k exact ⟨(m, n), h⟩
countable_uniontheoremApplies a library theorempropext, Classical.choice, Quot.sound
countable_unionLean 4Applies a library theoremFormally verified
/-- **A countable union of countable sets is countable** (Mathlib's `Set.countable_iUnion`; itsproof uses the axiom of choice, which is part of Lean's logic, to pick an enumeration of eachset). -/theorem countable_union {ι α : Type*} [Countable ι] (t : ι → Set α) (h : ∀ i, (t i).Countable) : (⋃ i, t i).Countable := Set.countable_iUnion h
cantortheoremProved here from basic factspropext, Classical.choice, Quot.sound
cantorLean 4Proved here from basic factsFormally verified
/-- **Cantor's theorem**: no function `f : A → 𝒫(A)` is surjective. The *diagonal set*`D = {a | a ∉ f a}` is missed: if `f a = D`, then `a ∈ D ↔ a ∉ f a ↔ a ∉ D`, which is impossible. -/theorem cantor {α : Type*} (f : α → Set α) : ¬ Surjective f := by intro hf obtain ⟨a, ha⟩ := hf {x | x ∉ f x} have h : a ∈ f a ↔ a ∉ f a := by constructor · intro hin rw [ha] at hin exact hin · intro hout rw [ha] exact hout by_cases hin : a ∈ f a · exact h.mp hin hin · exact hin (h.mpr hin)
/-- The **diagonal sequence** of a list `s₀, s₁, s₂, …` of infinite 0–1 sequences: its `n`-thentry is the opposite of the `n`-th entry of `sₙ`. -/def diagonal (s : ℕ → ℕ → Bool) : ℕ → Bool := fun n => !(s n n)
diagonal_netheoremProved here from basic factspropext
diagonal_neLean 4Proved here from basic factsFormally verified
/-- The diagonal sequence differs from the `n`-th sequence of the list — at position `n`. -/theorem diagonal_ne (s : ℕ → ℕ → Bool) (n : ℕ) : diagonal s ≠ s n := by intro h have hn : diagonal s n = s n n := congrFun h n unfold diagonal at hn cases hs : s n n <;> simp [hs] at hn
sequences_uncountabletheoremProved here from basic factspropext
sequences_uncountableLean 4Proved here from basic factsFormally verified
/-- **The infinite 0–1 sequences cannot be listed**: no `s : ℕ → (ℕ → Bool)` is surjective,because the diagonal sequence is never on the list. -/theorem sequences_uncountable : ¬ ∃ s : ℕ → (ℕ → Bool), Surjective s := by rintro ⟨s, hs⟩ obtain ⟨n, hn⟩ := hs (diagonal s) exact diagonal_ne s n hn.symm
/-- The careful **decimal diagonal**: from a list of digit sequences `rₙ = 0.rₙ₀ rₙ₁ rₙ₂…`, takedigit `5` in position `n` unless `rₙ` has a `5` there, in which case take `4`. -/def decimalDiagonal (r : ℕ → ℕ → Fin 10) : ℕ → Fin 10 := fun n => if r n n = 5 then 4 else 5
decimalDiagonal_spectheoremProved here from basic factspropext
decimalDiagonal_specLean 4Proved here from basic factsFormally verified
/-- The decimal diagonal (1) differs from the `n`-th expansion in the `n`-th digit, and (2) usesonly the digits `4` and `5` — never `0` or `9` — so it is the *only* decimal expansion of thenumber it names (no `…4999…`/`…5000…` ambiguity). -/theorem decimalDiagonal_spec (r : ℕ → ℕ → Fin 10) (n : ℕ) : decimalDiagonal r n ≠ r n n ∧ (decimalDiagonal r n = 4 ∨ decimalDiagonal r n = 5) := by unfold decimalDiagonal split_ifs with h · rw [h] exact ⟨by decide, Or.inl rfl⟩ · exact ⟨fun h' => h h'.symm, Or.inr rfl⟩
exists_transcendentaltheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_transcendentalLean 4Proved here from basic factsFormally verified
/-- **Transcendental numbers exist** — Cantor's 1874 argument. The real numbers that are roots ofnon-zero integer polynomials (the algebraic numbers) form a countable set (`Algebraic.countable`),but `ℝ` is uncountable, so some real number is not algebraic. The proof names no such number. -/theorem exists_transcendental : ∃ x : ℝ, Transcendental ℤ x := by by_contra h push Not at h apply real_uncountable apply (Algebraic.countable ℤ ℝ).mono intro x _ have hx := h x unfold Transcendental at hx exact not_not.mp hx
/-- The diagonal sequence `fun n => !(s n n)` differs from the `n`-th sequence of the list.Hint: `intro h`, evaluate both sides at `n` with `congrFun h n`, then split on the value of`s n n` with `cases hs : s n n` and `simp`. -/theorem diagonal_ne (s : ℕ → ℕ → Bool) (n : ℕ) : (fun k => !(s k k)) ≠ s n := by sorry
Show the compiled solution
diagonal_neLean 4Proved here from basic factsFormally verified
/-- The diagonal sequence differs from the `n`-th sequence of the list — at position `n`. -/theorem diagonal_ne (s : ℕ → ℕ → Bool) (n : ℕ) : diagonal s ≠ s n := by intro h have hn : diagonal s n = s n n := congrFun h n unfold diagonal at hn cases hs : s n n <;> simp [hs] at hn
/-- Cantor's theorem: no function from `α` to its power set is surjective.Hint: `intro hf`, then `obtain ⟨a, ha⟩ := hf {x | x ∉ f x}` and ask whether `a ∈ f a`. -/theorem cantor {α : Type*} (f : α → Set α) : ¬ Surjective f := by sorry
Show the compiled solution
cantorLean 4Proved here from basic factsFormally verified
/-- **Cantor's theorem**: no function `f : A → 𝒫(A)` is surjective. The *diagonal set*`D = {a | a ∉ f a}` is missed: if `f a = D`, then `a ∈ D ↔ a ∉ f a ↔ a ∉ D`, which is impossible. -/theorem cantor {α : Type*} (f : α → Set α) : ¬ Surjective f := by intro hf obtain ⟨a, ha⟩ := hf {x | x ∉ f x} have h : a ∈ f a ↔ a ∉ f a := by constructor · intro hin rw [ha] at hin exact hin · intro hout rw [ha] exact hout by_cases hin : a ∈ f a · exact h.mp hin hin · exact hin (h.mpr hin)