English
Given IsLocalHomeomorphOn f s and hs open, f''s is discrete if and only if s is discrete.
Русский
Дискретность образа при f''s равна дискретности s при выполнении условий.
LaTeX
$$$IsLocalHomeomorphOn\\, f\\, s \\land IsOpen s \\Rightarrow (DiscreteTopology (f'' s) \\iff DiscreteTopology s)$$$
Lean4
theorem discreteTopology_image_iff (h : IsLocalHomeomorphOn f s) (hs : IsOpen s) :
DiscreteTopology (f '' s) ↔ DiscreteTopology s :=
by
refine ⟨fun _ ↦ h.discreteTopology_of_image, ?_⟩
simp_rw [discreteTopology_iff_isOpen_singleton]
rintro hX ⟨_, x, hx, rfl⟩
obtain ⟨e, hxe, rfl⟩ := h x hx
refine ⟨e '' { x }, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩
· simpa using hs.isOpenMap_subtype_val _ (hX ⟨x, hx⟩)
· ext; simp [Subtype.ext_iff]