enumOfCountable

formal source

  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