decode₂_ne_none_iff — Mathlib

English

For Encodable α, decode₂ α n ≠ none if and only if n is in the range of encode.

Русский

Для кодируемого типа α, decode₂ α n ≠ none эквивалентно тому, что n лежит в образе encode.

LaTeX

$$$ \forall \alpha\ [Encodable(\alpha)],\forall n:\mathbb{N},\ decode_2(\alpha,n) \neq \mathrm{none} \iff n \in \mathrm{Set.range}(\mathrm{encode} : \alpha \to \mathbb{N})$$$

Lean4

theorem decode₂_ne_none_iff [Encodable α] {n : ℕ} : decode₂ α n ≠ none ↔ n ∈ Set.range (encode : α → ℕ) := by
  simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem, Encodable.mem_decode₂, not_forall,
    not_not]

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