decode_isSome — Mathlib

English

For every α with a denumerable structure, and every n ∈ ℕ, the decoding of n yields Some value.

Русский

Для любой денумерируемой структуры α и любого n ∈ ℕ декодирование n давaет Some некоторого значения.

LaTeX

$$$ (\text{decode}(\alpha := \alpha)\ n).isSome $$$

Lean4

theorem decode_isSome (α) [Denumerable α] (n : ℕ) : (decode (α := α) n).isSome :=
  Option.isSome_iff_exists.2 <| (decode_inv n).imp fun _ => And.left

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