English
For each natural length k and every predicate f on vectors of length k with entries in α, the statement that f holds for all such vectors is expressed by a curried universal quantification over the coordinates; i.e., f is true for every vector [x1, ..., xk] with xi ∈ α.
Русский
Для каждого натурального k и любого предиката f над векторами длины k над α утверждение, что f истинно для всех таких векторов, выражается через последовательный всеобщий квантор над координатами; то есть f истинно для каждого вектора [x1, ..., xk] с xi ∈ α.
LaTeX
$$$\mathrm{VectorAll}(k,f) \iff \forall (x_1,\dots,x_k) \in \alpha^k,\; f([x_1,\dots,x_k]).$$$
Lean4
/-- "Curried" forall, i.e. `∀ x₁ ... xₙ, f [x₁, ..., xₙ]`. -/
def VectorAll : ∀ k, (Vector3 α k → Prop) → Prop
| 0, f => f []
| succ k, f => ∀ x : α, VectorAll k fun v => f (x :: v)
