English
If f: X → Y is a local homeomorphism and f is surjective, then discrete topologies on X and Y coincide: X is discrete iff Y is discrete.
Русский
Если f: X → Y — локальная гомеоморфия и сюръективна, то дискретности X и Y эквивалентны: X дискретно тогда и только тогда, когда Y дискретно.
LaTeX
$$$\operatorname{IsLocalHomeomorph}(f) \\land \operatorname{Function.Surjective}(f) \\Rightarrow \bigl(\operatorname{DiscreteTopology}(X) \iff \operatorname{DiscreteTopology}(Y)\bigr)$$$
Lean4
/-- If there is a surjective local homeomorphism between two spaces and one of them is discrete,
then both spaces are discrete. -/
theorem discreteTopology_iff_of_surjective (h : IsLocalHomeomorph f) (hs : Function.Surjective f) :
DiscreteTopology X ↔ DiscreteTopology Y := by
rw [← (Homeomorph.Set.univ Y).discreteTopology_iff, ← hs.range_eq, h.discreteTopology_range_iff]
