not_specializes_infty_coe — Mathlib

English

The point at infinity does not specialize to any finite point: for all x in X, not Specializes ∞ to x.

Русский

Точка бесконечность не специализируется на какой-либо конечной точке: для всех x ∈ X не выполняется Specializes(∞, x).

LaTeX

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

Lean4

theorem not_specializes_infty_coe {x : X} : ¬Specializes ∞ (x : OnePoint X) :=
  isClosed_infty.not_specializes rfl (coe_ne_infty x)

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