English
Let G be a group and S a subset of G. The centralizer of the closure of S is the intersection, taken over all g in S, of the centralizers of the cyclic subgroups generated by g. In symbols: C_G(closure(S)) = ⋂_{g∈S} C_G(zpowers(g)).
Русский
Пусть G — группа, S ⊆ G. Централизатор замыкания S равен пересечению по всем эелементам g из S центральизаторов циклических подгрупп, порождаемых g.
LaTeX
$$$\mathrm{C}_G(\overline{S}) = \bigcap_{g \in S} \mathrm{C}_G(\mathrm{zpowers}(g))$$$
Lean4
@[to_additive]
theorem centralizer_closure (S : Set G) : centralizer (closure S : Set G) = ⨅ g ∈ S, centralizer (zpowers g : Set G) :=
le_antisymm (le_iInf fun _ => le_iInf fun hg => centralizer_le <| zpowers_le.2 <| subset_closure hg) <|
le_centralizer_iff.1 <|
(closure_le _).2 fun g => SetLike.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ iInf_le_of_le g ∘ iInf_le _
