adjoin_le_centralizer_centralizer

English

For any subset s, the adjoin of s is contained in the centralizer of the centralizer of s: adjoin_R s ≤ centralizer_R (centralizer_R s).

Русский

Для любого множества s порождение R содержится в центральизаторе двойном центральизаторе s: adjoin_R s ≤ centralizer_R(centralizer_R s).

LaTeX

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

Lean4

theorem adjoin_le_centralizer_centralizer (s : Set A) :
    adjoin R s ≤ Subalgebra.centralizer R (Subalgebra.centralizer R s) :=
  adjoin_le Set.subset_centralizer_centralizer

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