closure — Mathlib

English

The closure of a subset s of R is the smallest NonUnitalSubring of R containing s; equivalently, it is the intersection of all NonUnitalSubrings of R that contain s.

Русский

Замыкание множества s в R — наименьшее неединичное подполькo R, содержащее s; эквивалентно пересечению всех неединичных подпольр, содержащих s.

LaTeX

$$$\\mathrm{closure}(s) = \\bigcap \\{ S \\subseteq R \\mid S \\text{ is a NonUnitalSubring},\\ s \\subseteq S \\}$$$

Lean4

/-- The `NonUnitalSubring` generated by a set. -/
def closure (s : Set R) : NonUnitalSubring R :=
  sInf {S | s ⊆ S}

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