theorem
proved
enumOfCountable_surjective
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Shims.CountableEquiv on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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