closure_le_centralizer_centralizer

English

The closure of a set s inside a semiring sits inside the centralizer of the centralizer of s; i.e., closure(s) ≤ centralizer(centralizer(s)).

Русский

Замыкание множества s внутри полусемиринга лежит в центральизаторе центральизатора s: closure(s) ≤ centralizer(centralizer(s)).

LaTeX

$$$closure(s) \le\ centralizer(centralizer(s))$$$

Lean4

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

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