ne_infty_iff_exists — Mathlib

English

In the one-point compactification OnePoint X, an element x ∈ OnePoint X is different from the infinity point ∞ if and only if x is the image of some y ∈ X under the canonical embedding.

Русский

В одноточечной компактфикации OnePoint X элемент x ∈ OnePoint X отличается от бесконечности ∞ тогда и только тогда, когда x является образом некоторого y ∈ X через каноническое вложение.

LaTeX

$$$x \\neq \\infty \\;\\Longleftrightarrow\\; \\exists y:X,\\; (y:\\mathrm{OnePoint}\n X)=x.$$$

Lean4

theorem ne_infty_iff_exists {x : OnePoint X} : x ≠ ∞ ↔ ∃ y : X, (y : OnePoint X) = x := by
  induction x using OnePoint.rec <;> simp

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