toAddSubsemigroup_closure — Mathlib

English

The image of the closure of a set S under toAddSubsemigroup coincides with the closure of the preimage of S under Additive.toMul.

Русский

Образ замыкания множества S под преобразованием кAddSubsemigroup совпадает с замыканием предобраза S через Additive.toMul.

LaTeX

$$$\\text{AddSubsemigroup.toSubsemigroup}(\\text{Subsemigroup.closure } S) = \\text{Subsemigroup.closure}(\\text{Additive.toMul}^{-1}' S)$$$

Lean4

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

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