closure_eq — Mathlib

English

If S is a nonunital subsemiring of R, then closure of the carrier of S equals S itself.

Русский

Если S является неупорядоченным подполуссемирингом R, то замыкание множества его элементов равно самому S.

LaTeX

$$$\\operatorname{closure}(S) = S$$$

Lean4

/-- Closure of a non-unital subsemiring `S` equals `S`. -/
@[simp]
theorem closure_eq (s : NonUnitalSubsemiring R) : closure (s : Set R) = s :=
  (NonUnitalSubsemiring.gi R).l_u_eq s

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