cons — Mathlib

English

If f is Partrec' on n and g is Vec on n, then the function v ↦ List.Vector.cons (f v) (g v) is Partrec' on n.

Русский

Если f — Partrec' на n и g — Vec на n, то функция v ↦ cons (f v) (g v) есть Partrec' на n.

LaTeX

$$$$\forall \{n,m,f,g\},\; \mathrm{Nat.Partrec'}(f) \to \mathrm{Nat.Partrec'.Vec}(g) \to \mathrm{Nat.Partrec'.Vec}(\lambda v. \text{List.Vector.cons} (f v) (g v)).$$$$

Lean4

protected theorem cons {n m} {f : List.Vector ℕ n → ℕ} {g} (hf : @Partrec' n f) (hg : @Vec n m g) :
    Vec fun v => f v ::ᵥ g v := fun i => Fin.cases (by simpa using hf) (fun i => by simp only [hg i, get_cons_succ]) i

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