topologicalClosure_map — Mathlib

English

If f is a closed map, then the topological closure of the image equals the image of the topological closure.

Русский

Если отображение замкнуто, то замыкание образа равно образ замыкания.

LaTeX

$$map f.toAlgHom s.topologicalClosure = (map f.toAlgHom s).topologicalClosure$$

Lean4

theorem _root_.Subalgebra.topologicalClosure_map [IsTopologicalSemiring B] (f : A →A[R] B) (hf : IsClosedMap f)
    (s : Subalgebra R A) : (map f.toAlgHom s).topologicalClosure = map f.toAlgHom s.topologicalClosure :=
  SetLike.coe_injective <| hf.closure_image_eq_of_continuous f.continuous _

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