English
VectorAllP p v expresses that p holds for every coordinate of v, and it unfolds as a direct conjunction of p applied to each coordinate of the vector.
Русский
VectorAllP p v выражает, что p выполняется для каждой координаты вектора v, и разворачивается как прямая конъюнкция p(v_i) по всем координатам.
LaTeX
$$$\mathrm{VectorAllP}(p,v) \equiv \bigwedge_{i:\, Fin2(n)} p\bigl(v(i)\bigr).$$$
Lean4
/-- `VectorAllP p v` is equivalent to `∀ i, p (v i)`, but unfolds directly to a conjunction,
i.e. `VectorAllP p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
def VectorAllP (p : α → Prop) (v : Vector3 α n) : Prop :=
Vector3.recOn v True fun a v IH => @Vector3.recOn _ (fun _ => Prop) _ v (p a) fun _ _ _ => p a ∧ IH
