English
Any closed uncountable subset of a Polish space admits a continuous injection from Cantor space ℕ → Bool into the subset.
Русский
Любое замкнутое несчетное подмножество полиспеса допускает непрерывную инъекцию из Cantor пространства ℕ → Bool в это подмножество.
LaTeX
$$$\\exists f: (\\\\mathbb{N} \\\\to \\{0,1\\\\}) \\\\to C,\\ range(f) ⊆ C ∧ Continuous(f) ∧ Injective(f)$$$
Lean4
/-- Any closed uncountable subset of a Polish space admits a continuous injection
from the Cantor space `ℕ → Bool`. -/
theorem exists_nat_bool_injection_of_not_countable {α : Type*} [TopologicalSpace α] [PolishSpace α] {C : Set α}
(hC : IsClosed C) (hunc : ¬C.Countable) : ∃ f : (ℕ → Bool) → α, range f ⊆ C ∧ Continuous f ∧ Function.Injective f :=
by
letI := TopologicalSpace.upgradeIsCompletelyMetrizable α
obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc
obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty
exact ⟨f, hfD.trans hDC, hf⟩
