toSubsemigroup'_closure — Mathlib

English

The closure of Subsemigroup under toAddSubsemigroup' corresponds to the closure of AddSubsemigroup under Multiplicative.ofAdd.

Русский

Замыкание Subsemigroup под toAddSubsemigroup' соответствует замыканию AddSubsemigroup под Multiplicative.ofAdd.

LaTeX

$$$\\text{Subsemigroup.toAddSubsemigroup'}(\\text{Subsemigroup.closure } S) = \\text{AddSubsemigroup.closure}(\\text{Multiplicative.ofAdd}^{-1}' S)$$$

Lean4

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

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