toSubmonoid'_closure — Mathlib

English

For a set S in Multiplicative A, Submonoid.toAddSubmonoid'(Submonoid.closure S) equals AddSubmonoid.closure (Multiplicative.ofAdd^{-1} S).

Русский

Для множества S в Multiplicative A, Submonoid.toAddSubmonoid'(Submonoid.closure S) равняется AddSubmonoid.closure (Multiplicative.ofAdd^{-1} S).

LaTeX

$$$ Submonoid.toAddSubmonoid'(\mathrm{closure}(S)) = \mathrm{closure}(\mathrm{Multiplicative.ofAdd}^{-1} S) $$$

Lean4

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

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