mem_closure

Mathlib.Algebra.Ring.Subring.Basic

URI: https://scilib.ai/kg/mathlib#Subring.mem_closure

English

x ∈ closure s iff for all Subrings S with s ⊆ S, x ∈ S.

Русский

x принадлежит closure s тогда и только тогда, когда для каждого подкольца S с s ⊆ S, x ∈ S.

LaTeX

$$x ∈ closure s ↔ ∀ S : Subring R, s ⊆ S → x ∈ S$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru