toAddSubmonoid'_closure — Mathlib

English

Another articulation of the closure mapping between Submonoid and AddSubmonoid via Multiplicative A.

Русский

Еще одно изложение замыкания между Submonoid и AddSubmonoid через Multiplicative A.

LaTeX

$$$ \mathrm{toAddSubmonoid}'(\mathrm{closure}(S)) = \mathrm{closure}(\mathrm{Multiplicative.ofAdd}(S)) $$$

Lean4

theorem toAddSubmonoid'_closure (S : Set (Multiplicative A)) :
    Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (Multiplicative.ofAdd ⁻¹' S) :=
  le_antisymm
    (Submonoid.toAddSubmonoid'.to_galoisConnection.l_le <|
      Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := A))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := Multiplicative A))

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