decode_sigma_val — Mathlib

English

For encodable α with γ a family, the decoding of n for Sigma γ satisfies a formula using unpair(n).

Русский

Для кодируемого α с семейством γ, декодирование для Sigma γ удовлетворяет формуле через разбор n на (n1,n2).

LaTeX

$$$ \forall \alpha\, \forall \gamma:\alpha\to \mathrm{Type},\[Encodable\alpha],\forall n:\mathbb{N},\ (\mathrm{Encodable.decode}\ n) = ((\mathrm{Encodable.decode}\ (Nat.unpair\ n).fst).bind\ (\lambda a. \mathrm{Encodable.decode}\ (Nat.unpair\ n).snd).\text{map }(\Sigma.mk a))$$$

Lean4

@[simp]
theorem decode_sigma_val (n : ℕ) :
    (decode n : Option (Sigma γ)) = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Sigma.mk a :=
  rfl

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