canLift — Mathlib

English

There is a canonical lifting that identifies non-top elements of WithTop(α) with elements of α via untopped values, establishing a bijection between α and { y ∈ WithTop(α) | y ≠ ⊤ }.

Русский

Существует каноническое отображение, устанавливающее биекцию между α и множестом не-верхних элементов WithTop(α), задаваемое через untop.

LaTeX

$$$\{ y : \mathrm{WithTop}(\alpha) \mid y \neq \top \} \cong \alpha$$$

Lean4

instance canLift : CanLift (WithTop α) α (↑) fun r => r ≠ ⊤ where prf x h := ⟨x.untop h, coe_untop _ _⟩

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