lift — Mathlib

English

The lift operation converts a finite ENNat to a natural number, given a proof that it is finite.

Русский

Операция lift переводит конечный ENNat в натуральное число, имея доказательство конечности.

LaTeX

$$$$ \\text{lift}(x,h) \\in \\mathbb{N} \\quad\\text{and}\\quad x = \\text{the natural representation of } \\text{lift}(x,h). $$$$

Lean4

/-- Convert a `ℕ∞` to a `ℕ` using a proof that it is not infinite. -/
def lift (x : ℕ∞) (h : x < ⊤) : ℕ :=
  WithTop.untop x (WithTop.lt_top_iff_ne_top.mp h)

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