le_centralizer_centralizer — Mathlib

English

For any x, the elemental subalgebra is contained in the double centralizer of x.

Русский

Для любого x элементальная подпалгебра содержится во втором центральизаторе x.

LaTeX

$$$\\operatorname{elemental}_R(x) \\le \\operatorname{centralizer}_R(\\operatorname{centralizer}_R(\\{x\\}))$$$

Lean4

theorem le_centralizer_centralizer [T2Space A] (x : A) : elemental R x ≤ centralizer R (centralizer R { x }) :=
  topologicalClosure_adjoin_le_centralizer_centralizer ..

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