decode₂_eq_some — Mathlib

English

For Encodable α and any n ∈ ℕ and a ∈ α, decode₂ α n = some a if and only if encode a = n.

Русский

Для кодируемого типа α и любых n ∈ ℕ и a ∈ α, decode₂ α n = some a тогда же, когда encode a = n.

LaTeX

$$$ \forall \alpha\ [Encodable(\alpha)], \forall n:\mathbb{N}, \forall a:\alpha, \ decode_2(\alpha,n) = \mathrm{some}(a) \iff \mathrm{encode}(a) = n$$$

Lean4

theorem decode₂_eq_some [Encodable α] {n : ℕ} {a : α} : decode₂ α n = some a ↔ encode a = n :=
  mem_decode₂

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