English
A predicate holds for every vector of length n exactly when it holds for every coordinate of the vector, i.e., VectorAll p v is equivalent to ∀ i, p(v(i)).
Русский
Предикат выполняется для каждого вектора длины n тогда и только тогда, когда он выполняется для каждой координаты вектора: VectorAll p v ⇔ ∀ i, p(v(i)).
LaTeX
$$$\mathrm{VectorAllP}(p,v) \iff \forall i:\mathrm{Fin2}(n),\; p(v(i)).$$$
Lean4
theorem vectorAll_iff_forall : ∀ {n} (f : Vector3 α n → Prop), VectorAll n f ↔ ∀ v, f v
| 0, _ => ⟨fun f0 v => v.nilElim f0, fun al => al []⟩
| succ _, f =>
(forall_congr' fun x => vectorAll_iff_forall fun v => f (x :: v)).trans
⟨fun al v => v.consElim al, fun al x v => al (x :: v)⟩
