English
There is an equivalence between FinVec.Exists P and the plain existential: FinVec.Exists P is equivalent to ∃ x, P x; this is an improved, definitional form of existence for vectors.
Русский
Существует эквивалентность между FinVec.Exists P и простым существованием: FinVec.Exists P эквивалентно ∃ x, P x.
LaTeX
$$$\forall {m} (P : (Fin m \to \alpha) \to Prop),\; FinVec.Exists P \;\iff\; \exists x, P x$$$
Lean4
/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∃ f, P f) ↔ ∃ a₀ a₁, P ![a₀, a₁] :=
(exists_iff _).symm
```
-/
theorem exists_iff : ∀ {m} (P : (Fin m → α) → Prop), Exists P ↔ ∃ x, P x
| 0, P => by
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
rfl
| .succ n, P => by simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]
