topologicalClosure_adjoin_le_centralizer_centralizer

English

In a T2-space, the topological closure of the subalgebra generated by a set s is contained in the centralizer of the centralizer of s.

Русский

В пространстве T2 замыкание алгебры, порожденной множеством s, содержится в центральизаторе центральизатора s.

LaTeX

$$In a T2-space, $\overline{\mathrm{adjoin}_R(s)} \le \mathrm{centralizer}_R( \mathrm{centralizer}_R(s))$$$

Lean4

theorem topologicalClosure_adjoin_le_centralizer_centralizer [T2Space A] (s : Set A) :
    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

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