isClosedMap_iff_comap_nhds_le — Mathlib

English

Equivalence of closed map with comap nhds for pointwise nhds.

Русский

Замкнутое отображение эквивалентно равенству comap nhds на точки.

LaTeX

$$$IsClosedMap f \\iff ∀ y:Y, comap f (\\mathcal{N} y) ≤ \\mathcal{N}^\ast (f^{-1} {y})$$$

Lean4

theorem isClosedMap_iff_comap_nhds_le : IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' { y }) :=
  by
  rw [isClosedMap_iff_comap_nhdsSet_le]
  constructor
  · exact fun H y ↦ nhdsSet_singleton (x := y) ▸ H
  · intro H s
    rw [← Set.biUnion_of_singleton s]
    simp_rw [preimage_iUnion, nhdsSet_iUnion, comap_iSup, nhdsSet_singleton]
    exact iSup₂_mono fun _ _ ↦ H

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