topologicalClosure_adjoin_le_centralizer_centralizer

English

For any subset s ⊆ A, the topological closure of the subalgebra generated by s is contained in the centralizer of the centralizer of s: cl(adjoin_R(s)) ⊆ centralizer_R(centralizer_R(s)).

Русский

Для любого подмножества s ⊆ A топологическое замыкание подалгебры, сгенерированной этим множеством, содержится в центральизаторе двойного центральизатора: cl(adjoin_R(s)) ⊆ centralizer_R(centralizer_R(s)).

LaTeX

$$$\overline{\operatorname{adjoin}_R(s)} \le \operatorname{centralizer}_R\big(\operatorname{centralizer}_R(s)\big)$$$

Lean4

theorem topologicalClosure_adjoin_le_centralizer_centralizer [IsScalarTower R A A] [SMulCommClass R A A] [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 _)

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