specializes_rfl

Mathlib.Topology.Inseparable

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

English

x specializes to y if and only if y lies in closure of {x}.

Русский

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

LaTeX

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

Lean4

theorem specializes_rfl : x ⤳ x :=
  le_rfl

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

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

Разделы

Аффилиация

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