English
For every m, n and predicate P on m×n matrices, Exists P holds if and only if there exists a matrix X with P(X).
Русский
Для любых m, n и предиката P над матрицами размерности m×n выполняется: Exists P эквивалентно существованию матрицы X с P(X).
LaTeX
$$Exists P \\leftrightarrow \\exists X, P(X)$$
Lean4
/-- This can be used to prove
```lean
example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
(∃ x, P x) ↔ ∃ a b c d e f, P !![a, b, c; d, e, f] :=
(exists_iff _).symm
```
-/
theorem exists_iff : ∀ {m n} (P : Matrix (Fin m) (Fin n) α → Prop), Exists P ↔ ∃ x, P x
| 0, _, _ => Iff.symm Fin.exists_fin_zero_pi
| m + 1, n, P => by
simp only [Exists, FinVec.exists_iff, exists_iff]
exact Iff.symm Fin.exists_fin_succ_pi
