IndisputableMonolith.Shims.CountableEquiv

   1import Mathlib
   2
   3/-!
   4Shims for countability and equivalence constructions that are convenient
   5for Lean 4 developments.
   6
   7Provides:
   8- `enumOfCountable` to get a surjection `ℕ → α` from `Countable α`.
   9- `countable_of_surjective` to obtain `Countable α` from a surjection `ℕ → α`.
  10
  11## Implementation Notes
  12
  13mathlib's `Countable` API is stable but indirect (works via `Encodable` or injections).
  14For clarity and to avoid version coupling, we provide clean constructive proofs here.
  15-/
  16
  17open Classical
  18open Function
  19
  20namespace Shims
  21
  22universe u
  23
  24/-! ### Countability from surjection (fully proven) -/
  25
  26theorem countable_of_surjective {α : Type u} (f : ℕ → α) (hf : Surjective f) : Countable α := by
  27  -- Build an injection α → ℕ from the surjection
  28  classical
  29  let g : α → ℕ := fun a => Nat.find (hf a)
  30  have hg : ∀ a, f (g a) = a := fun a => Nat.find_spec (hf a)
  31  -- g is a left inverse, hence injective
  32  have hinj : Injective g := by
  33    intro a₁ a₂ heq
  34    calc a₁ = f (g a₁) := (hg a₁).symm
  35      _ = f (g a₂) := by rw [heq]
  36      _ = a₂ := hg a₂
  37  -- Use mathlib's Countable constructor (exists in Lean 4)
  38  exact ⟨g, hinj⟩
  39
  40/-! ### Enumeration from countability -/
  41
  42/-- From `Countable α` and inhabitedness, produce a surjection `ℕ → α`.
  43
  44**Proof strategy**: Use `Nonempty.some` to extract the injection witness from `Countable`,
  45then invert it classically to build a surjection.
  46
  47The challenge is that `Countable α := ∃ f, Injective f` is in `Prop`, but we need
  48to use the witness `f` in a `Type`-producing definition. We use `Nonempty` coercion. -/
  49noncomputable def enumOfCountable {α : Type u} [Inhabited α] (h : Countable α) : ℕ → α :=
  50  -- Convert existence proof to Nonempty, then extract witness
  51  let f_witness : Nonempty (∃ f : α → ℕ, Injective f) := ⟨h.exists_injective_nat⟩
  52  let f_data := Classical.choice f_witness
  53  let f := f_data.choose
  54  -- Build surjection by choosing preimages
  55  fun n => if h : ∃ a, f a = n then Classical.choose h else default
  56
  57theorem enumOfCountable_surjective {α : Type u} [Inhabited α] (h : Countable α) :
  58    Function.Surjective (enumOfCountable h) := by
  59  intro a
  60  classical
  61  -- Extract the injection
  62  let f_witness : Nonempty (∃ f : α → ℕ, Injective f) := ⟨h.exists_injective_nat⟩
  63  let f_data := Classical.choice f_witness
  64  let f := f_data.choose
  65  let hinj := f_data.choose_spec
  66  -- f a is in the range, so enumOfCountable (f a) = a
  67  use f a
  68  simp [enumOfCountable]
  69  have hex : ∃ a', f a' = f a := ⟨a, rfl⟩
  70  rw [dif_pos hex]
  71  have hchoose := Classical.choose_spec hex
  72  exact hinj hchoose
  73
  74end Shims
  75