map_decode_iff — Mathlib

English

Computability of a map-composed decoding is equivalent to computability of the original map, via decode and map transformations.

Русский

Вычислимость отображения после декодирования равносильна вычислимости исходного отображения через соответствующие преобразования декодирования и отображения.

LaTeX

$$$\mathrm{Computable}_2 f \iff \mathrm{Computable}_2 (\lambda a\ n. \mathrm{decode}(n).map (f\ a))$$$

Lean4

theorem map_decode_iff {f : α → β → σ} : (Computable₂ fun a n => (decode (α := β) n).map (f a)) ↔ Computable₂ f :=
  by
  convert (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff
  apply Option.map_eq_bind

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