encodable — Mathlib

English

For encodable types α and β, decoding the encoded sum returns the original sum when composed with the encoding.

Русский

Для кодируемых типов α и β декодирование кодирования суммы возвращает исходную сумму при компоновке с кодированием.

LaTeX

$$$ \forall s:\mathrm{Sum}(\alpha,\beta),\ \mathrm{decodeSum}(\mathrm{encodeSum}(s)) = \mathrm{Option.some}(s)$$$

Lean4

/-- If `α` and `β` are encodable, then so is their sum. -/
instance _root_.Sum.encodable : Encodable (α ⊕ β) :=
  ⟨encodeSum, decodeSum, fun s => by cases s <;> simp [encodeSum, div2_val, decodeSum, encodek]⟩

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