coe_closure_eq — Mathlib

English

The underlying set of closure s equals AddSubmonoid.closure of Subsemigroup.closure s.

Русский

Множество closure s равно AddSubmonoid.closure( Subsemigroup.closure s ).

LaTeX

$$(closure s : Set R) = AddSubmonoid.closure (Subsemigroup.closure s : Set R)$$

Lean4

/-- The elements of the non-unital subsemiring closure of `M` are exactly the elements of the
additive closure of a multiplicative subsemigroup `M`. -/
theorem coe_closure_eq (s : Set R) : (closure s : Set R) = AddSubmonoid.closure (Subsemigroup.closure s : Set R) := by
  simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

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