decode_eq_ofNat — Mathlib

English

For every α denumerable and n, decoding yields exactly the value of ofNat: decode α n = some (ofNat α n).

Русский

Для денумеруемого α и каждого n декаодирование даёт ровно значение ofNat α n: decode α n = some (ofNat α n).

LaTeX

$$$ \text{decode}(\alpha := \alpha)\ n = \text{Some } (\text{ofNat } α n) $$$

Lean4

@[simp]
theorem decode_eq_ofNat (α) [Denumerable α] (n : ℕ) : decode (α := α) n = some (ofNat α n) :=
  Option.eq_some_of_isSome _

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