topologicalClosure_map — Mathlib

English

If φ is a closed map and continuous, then the closure of the image equals the image of the closure: (map φ s).topologicalClosure = map φ s.topologicalClosure.

Русский

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

LaTeX

$$$(map\ φ\ s).topologicalClosure = map\ φ\ s.topologicalClosure$$$

Lean4

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

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