vec_iff — Mathlib

English

A function f: List.Vector Nat m → List.Vector Nat n is computable if and only if its vector-encoded representation Vec f is computable.

Русский

Функция f: List.Vector Nat m → List.Vector Nat n вычислима тогда и только тогда, когда её векторное представление Vec f вычислимо.

LaTeX

$$$ \forall m n f:\; (\text{List.Vector Nat } m \to \text{List.Vector Nat } n),\; @Vec m n f \iff Computable f $$$

Lean4

theorem vec_iff {m n f} : @Vec m n f ↔ Computable f :=
  ⟨fun h => by simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i), fun h i =>
    of_part <| vector_get.comp h (const i)⟩

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