isClosedMap_iff_comap_nhdsSet_le — Mathlib

English

Equivalence of closed map with comap-nhdsSet inequality.

Русский

Эквивалентность замкнутости отображения с неравенством comap-nhdsSet.

LaTeX

$$$IsClosedMap f \\iff ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f^{-1} s)$$$

Lean4

theorem isClosedMap_iff_comap_nhdsSet_le : IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s) :=
  by
  simp_rw [Filter.le_def, mem_comap'', ← subset_interior_iff_mem_nhdsSet, ← subset_kernImage_iff,
    isClosedMap_iff_kernImage_interior]
  exact ⟨fun H s t hst ↦ hst.trans H, fun H s ↦ H _ subset_rfl⟩

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