infty_notMem_range_coe

Mathlib.Topology.Compactification.OnePoint.Basic

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

English

The point at infinity is not in the image of X under the inclusion i: X → OnePoint X.

Русский

Точка бесконечности ∞ не принадлежит образу X под вложением i: X → OnePoint X.

LaTeX

$$$\\infty \\notin i''X.$$$

Lean4

theorem infty_notMem_range_coe : ∞ ∉ range ((↑) : X → OnePoint X) :=
  notMem_range_coe_iff.2 rfl

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

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

Разделы

Аффилиация

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