discreteTopology_image_iff — Mathlib

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]

Похожие утверждения