toAddSubmonoid_closure — Mathlib

English

Same as previous: closure correspondence between Submonoid and AddSubmonoid via Additive translation.

Русский

То же самое: соответствие замыкания между Submonoid и AddSubmonoid через перевод Additive.

LaTeX

$$$ \mathrm{toAddSubmonoid}(\mathrm{closure}(S)) = \mathrm{closure}(\mathrm{Additive.toMul}^{-1} S) $$$

Lean4

theorem toAddSubmonoid_closure (S : Set M) :
    Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (Additive.toMul ⁻¹' S) :=
  le_antisymm
    (Submonoid.toAddSubmonoid.le_symm_apply.1 <| Submonoid.closure_le.2 (AddSubmonoid.subset_closure (M := Additive M)))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := M))

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