canLift — Mathlib

English

There exists a canonical CanLift structure from WithBot α to α on non-bottom elements, enabling to recover the underlying element from a non-bottom with proof.

Русский

Существует каноническая структура CanLift от WithBot α к α на не-низших элементах, позволяющая восстановить исходный элемент по не-нулевому элементу с доказательством.

LaTeX

$$$\text{CanLift} (WithBot \ α) α (↑) (\ \text{non-bottom})$$$

Lean4

instance canLift : CanLift (WithBot α) α (↑) fun r => r ≠ ⊥ where prf x h := ⟨x.unbot h, coe_unbot _ _⟩

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