canLift — Mathlib

English

Any monotone function α → β can be lifted to an OrderHom α β.

Русский

Любую монотонную функцию можно поднять до упакованного отображения порядка OrderHom α β.

LaTeX

$$$\\text{CanLift}(\\alpha \\to β) (\\alpha \\to_o β) \\uparrow Monotone$; witness: $f,h \\mapsto ⟨⟨f,h⟩, rfl⟩$$$

Lean4

/-- One can lift an unbundled monotone function to a bundled one. -/
protected instance canLift : CanLift (α → β) (α →o β) (↑) Monotone where prf f h := ⟨⟨f, h⟩, rfl⟩

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