countable_of_surjective

formal source

  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