canLift — Mathlib

English

There exists a partial inverse of the embedding i: X → OnePoint X on the non-infinity part, i.e., a map π defined on i(X) with π(i(x)) = x for all x ∈ X.

Русский

Существует частичный обратный к вложению i: X → OnePoint X на области, не содержащей ∞, то есть отображение π на i(X) такое, что π(i(x)) = x для всех x ∈ X.

LaTeX

$$$\\exists \\pi: \\mathrm{OnePoint} X \\dashrightarrow X \\text{ such that } \\pi(\\iota(x))=x \\text{ for all } x\\in X.$$$

Lean4

instance canLift : CanLift (OnePoint X) X (↑) fun x => x ≠ ∞ :=
  WithTop.canLift

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