instEncodableOfSigmaNatFunctions — Mathlib

English

Provided α and Σ i, L.Functions i are encodable, L.Term α is encodable.

Русский

Если α и Σ i, L.Functions i кодируемы, то L.Term α кодируемы.

LaTeX

$$$[Encodable\; α] \Rightarrow [Encodable\; (L.Term α)]$$$

Lean4

instance [Encodable α] [Encodable (Σ i, L.Functions i)] : Encodable (L.Term α) :=
  Encodable.ofLeftInjection listEncode (fun l => (listDecode l).head?.join) fun t =>
    by
    simp only
    rw [← flatMap_singleton listEncode, listDecode_encode_list]
    simp only [Option.join, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some, id_eq]

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