topologicalClosure_map — Mathlib

English

If φ is a closed map and continuous, then φ commutes with topological closure: φ(cl(s)) = cl(φ(s)).

Русский

Если отображение φ замкнутое и непрерывное, то оно сохраняет топологическое замыкание: φ(cl(s)) = cl(φ(s)).

LaTeX

$$$\phi(\overline{S}) = \overline{\phi(S)}$$$

Lean4

theorem topologicalClosure_map (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

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