isClosedMap_iff_closure_image — Mathlib

English

IsClosedMap f is equivalent to an inequality between comap and nhds: comap f (𝓝 y) ≤ 𝓝ˢ (f⁻¹{y}) for all y.

Русский

IsClosedMap f эквивалентно неравенству между comap и nhds: comap f (𝓝 y) ≤ 𝓝ˢ (f⁻¹{y}) для всех y.

LaTeX

$$$IsClosedMap f \\iff ∀ {y:Y}, \\ comap f (𝓝 y) \\le 𝓝ˢ (f^{-1} {y})$$$

Lean4

theorem isClosedMap_iff_closure_image : IsClosedMap f ↔ ∀ s, closure (f '' s) ⊆ f '' closure s :=
  ⟨IsClosedMap.closure_image_subset, fun hs c hc =>
    isClosed_of_closure_subset <|
      calc
        closure (f '' c) ⊆ f '' closure c := hs c
        _ = f '' c := by rw [hc.closure_eq]⟩

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