English
VectorAllP p v is equivalent to saying that p holds for every coordinate of v, i.e., ∀ i, p (v i).
Русский
VectorAllP p v эквивалентно тому, что для каждой координаты v выполняется p, то есть ∀ i, p(v i).
LaTeX
$$$\mathrm{VectorAllP}(p,v) \iff \forall i:\, Fin2(n),\; p(v(i)).$$$
Lean4
theorem vectorAllP_iff_forall (p : α → Prop) (v : Vector3 α n) : VectorAllP p v ↔ ∀ i, p (v i) :=
by
refine v.recOn ?_ ?_
· exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
· simp only [vectorAllP_cons]
refine fun {n} a v IH =>
(and_congr_right fun _ => IH).trans
⟨fun ⟨pa, h⟩ i => by
refine i.cases' ?_ ?_
exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩
· simpa using h fz
· simpa using h (fs i)
