le_centralizer_centralizer — Mathlib

English

For any x, elemental R x ≤ centralizer R (centralizer R { x }).

Русский

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

LaTeX

$$elemental R x ≤ centralizer R (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 ..

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