mem_closure — Mathlib

English

Membership in closure s is characterized by a universal property: x ∈ closure s iff for every NonUnitalSubring S with s ⊆ S we have x ∈ S.

Русский

Членство x в замыкании s характеризуется универсальным свойством: x ∈ closure(s) тогда и только тогда, когда для каждого NonUnitalSubring S, содержащего s, имеется x ∈ S.

LaTeX

$$$x \\in \\mathrm{closure}(s) \\iff \\forall S : \\mathrm{NonUnitalSubring}(R),\\ s \\subseteq S \\rightarrow x \\in S$$$

Lean4

theorem mem_closure {x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : NonUnitalSubring R, s ⊆ S → x ∈ S :=
  mem_sInf

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