le_centralizer_centralizer — Mathlib

English

For any subset s of R, s is contained in the centralizer of the centralizer of s; i.e., s ⊆ centralizer(centralizer(s)).

Русский

Для любого подмножества s в R выполняется s ⊆ centralizer(centralizer(s)).

LaTeX

$$$s \\subseteq \\operatorname{centralizer}(\\operatorname{centralizer}(s))$$$

Lean4

theorem le_centralizer_centralizer {R} [Semiring R] {s : Subsemiring R} : s ≤ centralizer (centralizer (s : Set R)) :=
  Set.subset_centralizer_centralizer

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