theorem
proved
term proof
enumOfCountable_surjective
show as:
view Lean formalization →
formal statement (Lean)
57theorem enumOfCountable_surjective {α : Type u} [Inhabited α] (h : Countable α) :
58 Function.Surjective (enumOfCountable h) := by
proof body
Term-mode proof.
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