English
The closure of a Subsemigroup of Multiplicative A under toAddSubsemigroup' equals AddSubsemigroup.closure of the preimage under Multiplicative.ofAdd.
Русский
Замыкание подполугруппы Multiplicative A под toAddSubsemigroup' эквивалентно замыканию AddSubsemigroup через предобраз Multiplicative.ofAdd.
LaTeX
$$$\\text{Subsemigroup.toAddSubsemigroup'}(\\text{Subsemigroup.closure } S) = \\text{AddSubsemigroup.closure}(\\text{Multiplicative.ofAdd}^{-1} S)$$$
Lean4
theorem toAddSubsemigroup'_closure (S : Set (Multiplicative A)) :
Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (Multiplicative.ofAdd ⁻¹' S) :=
le_antisymm
(Subsemigroup.toAddSubsemigroup'.to_galoisConnection.l_le <|
Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))
(AddSubsemigroup.closure_le.2 <| Subsemigroup.subset_closure (M := Multiplicative A))
