mem_decode₂' — Mathlib

English

For any a, a ∈ decode₂ α n iff a ∈ decode n and encode a = n.

Русский

Для любого a, a входит в decode₂ α n тогда и только тогда, когда a ∈ decode n и encode a = n.

LaTeX

$$$a \\in \\mathrm{decode}_2(\\alpha)(n) \\iff a \\in \\mathrm{decode}(n) \\land \\mathrm{encode}(a) = n.$$$

Lean4

theorem mem_decode₂' [Encodable α] {n : ℕ} {a : α} : a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n := by
  simp [decode₂, Option.bind_eq_some_iff]

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