mem_decode₂ — Mathlib

English

Let α be an encodable type. For every n ∈ ℕ and a ∈ α, a ∈ decode₂ α n if and only if encode a = n.

Русский

Пусть α — кодируемый тип. Для каждого n ∈ ℕ и a ∈ α верно: a принадлежит decode₂ α n тогда и только тогда, когда encode a = n.

LaTeX

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

Lean4

theorem mem_decode₂ [Encodable α] {n : ℕ} {a : α} : a ∈ decode₂ α n ↔ encode a = n :=
  mem_decode₂'.trans (and_iff_right_of_imp fun e => e ▸ encodek _)

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