topologicalClosure_map_le — Mathlib

English

For a ring hom f that is closed, the image of the closure is contained in the closure of the image.

Русский

Для замкнутого отображения f образ замыкания сопоставим с замыканием образа.

LaTeX

$$[IsClosedMap f →] (s) topologicalClosure ≤ map f s.topologicalClosure$$

Lean4

theorem _root_.Subalgebra.topologicalClosure_map_le [IsTopologicalSemiring B] (f : A →ₐ[R] B) (hf : IsClosedMap f)
    (s : Subalgebra R A) : (map f s).topologicalClosure ≤ map f s.topologicalClosure :=
  hf.closure_image_subset _

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