def
definition
def or abbrev
enumOfCountable
show as:
view Lean formalization →
formal statement (Lean)
49noncomputable def enumOfCountable {α : Type u} [Inhabited α] (h : Countable α) : ℕ → α :=
proof body
Definition body.
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