ofNat — Mathlib

English

For a denumerable α, the nth element is obtained by decoding and taking the corresponding value.

Русский

Для денумерируемого типа α n-й элемент получается путём декодирования и выбора соответствующего значения.

LaTeX

$$$ \text{ofNat}(\alpha,n) = x \quad\text{where}\quad \text{decode}(\alpha,n) = \text{Some } x $$$

Lean4

/-- Returns the `n`-th element of `α` indexed by the decoding. -/
def ofNat (α) [Denumerable α] (n : ℕ) : α :=
  Option.get _ (decode_isSome α n)

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