toAddSubgroup_closure — Mathlib

English

The AddSubgroup closure of S corresponds to the Subgroup closure of the preimage under Multiplicative.toAdd.

Русский

Замыкание AddSubgroup S эквивалентно замыканию Subgroup от предобраза S через Multiplicative.toAdd.

LaTeX

$$$ (\mathrm{AddSubgroup.closure} S) .\mathrm{toSubgroup} = \mathrm{Subgroup.closure}(\mathrm{Multiplicative.toAdd}^{-1} S) $$$

Lean4

theorem toAddSubgroup_closure (S : Set G) :
    (Subgroup.closure S).toAddSubgroup = AddSubgroup.closure (Additive.toMul ⁻¹' S) :=
  le_antisymm (toAddSubgroup.le_symm_apply.mp <| (closure_le _).mpr (AddSubgroup.subset_closure (G := Additive G)))
    ((AddSubgroup.closure_le _).mpr (subset_closure (G := G)))

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