canLift — Mathlib

English

There is a canonical embedding of Interval α into NonemptyInterval α, defined by the condition r ≠ ⊥; this is captured by a CanLift instance.

Русский

Существует каноническое вложение Interval α в NonemptyInterval α, определяемое условием r ≠ ⊥; это формализовано через экземпляр CanLift.

LaTeX

$$$\text{CanLift}(\mathrm{Interval}(\alpha), \mathrm{NonemptyInterval}(\alpha), \uparrow, \lambda r. r \neq \bot)$$$

Lean4

instance canLift : CanLift (Interval α) (NonemptyInterval α) (↑) fun r => r ≠ ⊥ :=
  WithBot.canLift

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