closure_subsemigroup_closure — Mathlib

English

closure of the underlying set of Subsemigroup.closure s equals closure s as a nonunital subsemiring.

Русский

Замыкание множества Subsemigroup.closure s равно closure s как неединичный подсемиринг.

LaTeX

$$closure( Subsemigroup.closure s ) = closure s$$

Lean4

@[simp]
theorem closure_subsemigroup_closure (s : Set R) : closure ↑(Subsemigroup.closure s) = closure s :=
  le_antisymm (closure_le.mpr fun _ hy => (Subsemigroup.mem_closure.mp hy) (closure s).toSubsemigroup subset_closure)
    (closure_mono Subsemigroup.subset_closure)

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