English
For any n, a predicate f on vectors of length n satisfies that there exists a vector with f if and only if there exists a vector v with f(v).
Русский
Для любого n предикат f над векторами длины n выполняется равносильность: существует вектор с свойством f ⇔ существует вектор v, такой что f(v).
LaTeX
$$$\mathrm{VectorEx}(n,f) \iff \exists v: Vector3(\alpha,n), f(v).$$$
Lean4
theorem vectorEx_iff_exists : ∀ {n} (f : Vector3 α n → Prop), VectorEx n f ↔ Exists f
| 0, f => (exists_vector_zero f).symm
| succ _, f => Iff.trans (exists_congr fun _ => vectorEx_iff_exists _) (exists_vector_succ f).symm