toSubsemigroup_closure — Mathlib

English

The closure of an additive subsemigroup corresponds to the closure of a subsemigroup under Multiplicative.toAdd.

Русский

Замыкание аддитивной подполугруппы соответствует замыканию подполугруппы под Multiplicative.

LaTeX

$$$\\text{AddSubsemigroup.toSubsemigroup}(\\text{AddSubsemigroup.closure } S) = \\text{Subsemigroup.closure}(\\text{Multiplicative.toAdd} \\^{-1} S)$$$

Lean4

theorem toSubsemigroup_closure (S : Set A) :
    AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (Multiplicative.toAdd ⁻¹' S) :=
  le_antisymm
    (AddSubsemigroup.toSubsemigroup.to_galoisConnection.l_le <|
      AddSubsemigroup.closure_le.2 <| Subsemigroup.subset_closure (M := Multiplicative A))
    (Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))

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