English
Under a local homeomorph on s, discreteness of f''s is equivalent to discreteness of s, provided openness of s.
Русский
При локальном гомеоморфизме на s дискретность образа f''s эквивалентна дискретности s при условии, что s открыто.
LaTeX
$$$IsLocalHomeomorphOn\\, f\\, s\\Rightarrow IsOpen(s)\\Rightarrow (DiscreteTopology (f'' s) \\iff DiscreteTopology s)$$$
Lean4
theorem discreteTopology_of_image (h : IsLocalHomeomorphOn f s) [DiscreteTopology (f '' s)] : DiscreteTopology s :=
discreteTopology_iff_isOpen_singleton.mpr fun x ↦
by
obtain ⟨e, hx, rfl⟩ := h x x.2
have ⟨U, hU, eq⟩ := isOpen_discrete {(⟨_, _, x.2, rfl⟩ : e '' s)}
refine
⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩
· exact Subtype.ext_iff.mp (eq.subset (a := ⟨_, x', x'.2, rfl⟩) mem.2)
· rintro x rfl; exact ⟨hx, eq.superset rfl⟩
