English
If f is a local homeomorphism on s and f''s is discrete, then s has the discrete topology.
Русский
Если f локальный гомеоморфизм на s и образ f''s дискретен, то s дискретна.
LaTeX
$$$IsLocalHomeomorphOn\\, f\\, s \\implies [DiscreteTopology (f'' s)]->DiscreteTopology s$$$
Lean4
theorem isLocalHomeomorphOn_iff_isOpenEmbedding_restrict {f : X → Y} :
IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f) :=
by
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
· obtain ⟨e, hxe, rfl⟩ := h x hx
exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩
· obtain ⟨U, hU, emb⟩ := h x hx
have : IsOpenEmbedding ((interior U).restrict f) :=
by
refine emb.comp ⟨.inclusion interior_subset, ?_⟩
rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
haveI : Nonempty X := ⟨x⟩
exact
⟨OpenPartialHomeomorph.ofContinuousOpenRestrict (Set.injOn_iff_injective.mpr inj).toPartialEquiv
(continuousOn_iff_continuous_restrict.mpr cont) openMap isOpen_interior,
mem_interior_iff_mem_nhds.mpr hU, rfl⟩
