vectorEx_iff_exists — Mathlib

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

Похожие утверждения