not_inseparable_infty_coe

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.not_inseparable_infty_coe

English

For any finite point x ∈ X, ∞ is not inseparable from x.

Русский

Для любой конечной точки x ∈ X ∞ не является неразделимым с x.

LaTeX

$$$\\forall x \\in X, \\neg \\operatorname{Inseparable}(\\infty, x).$$$

Lean4

theorem not_inseparable_infty_coe {x : X} : ¬Inseparable ∞ (x : OnePoint X) := fun h =>
  not_specializes_infty_coe h.specializes

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

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

Разделы

Аффилиация

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