closure_le_centralizer_centralizer

English

The closure of any set is contained in the centralizer of the centralizer of that set.

Русский

Замыкание множества входит в центральизатор центральизатора этого множества.

LaTeX

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

Lean4

@[to_additive]
theorem closure_le_centralizer_centralizer (s : Set M) : closure s ≤ centralizer (centralizer s) :=
  closure_le.mpr Set.subset_centralizer_centralizer

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