closure_le_centralizer_centralizer

English

Let S be a subset of a group G. Then the subgroup generated by S lies inside the centralizer of the centralizer of S.

Русский

Пусть S ⊆ G. Тогда порожденная S подгруппа содержится в центральизаторе центральизатора S.

LaTeX

$$$\langle S\rangle \le C_G\big(C_G(S)\big)$$$

Lean4

@[to_additive]
theorem closure_le_centralizer_centralizer (s : Set G) : closure s ≤ centralizer (centralizer s) :=
  closure_le _ |>.mpr Set.subset_centralizer_centralizer

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