closure_le_centralizer_centralizer

English

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

Русский

Для любого подмножества s ⊆ R замыкание s содержится в двойном централизаоре: closure(s) ⊆ centralizer(centralizer(s)).

LaTeX

$$$\\mathrm{closure}(s) \\le \\mathrm{centralizer}(\\mathrm{centralizer}(s))$$$

Lean4

theorem closure_le_centralizer_centralizer (s : Set R) : closure s ≤ centralizer (centralizer s) :=
  closure_le.mpr Set.subset_centralizer_centralizer

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