topologicalClosure_coe — Mathlib

English

Under a closed map, the image of the topological closure is contained in the topological closure of the image.

Русский

При замкнутом отображении образ замыкания изображения содержится в замыкании образа.

LaTeX

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

Lean4

@[simp]
theorem _root_.Subalgebra.topologicalClosure_coe (s : Subalgebra R A) : (s.topologicalClosure : Set A) = closure ↑s :=
  rfl

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