specializes_iff_mem_closure

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#specializes_iff_mem_closure

English

x specializes to y if and only if y belongs to the closure of {x}.

Русский

x специализируется на y тогда, когда y принадлежит замыканию множества {x}.

LaTeX

$$$ x ⤳ y \iff y \in \operatorname{closure}(\{x\})$$$

Lean4

theorem specializes_iff_mem_closure : x ⤳ y ↔ y ∈ closure ({ x } : Set X) :=
  (specializes_TFAE x y).out 0 4

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

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

Разделы

Аффилиация

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