exists_vector_zero — Mathlib

English

For a predicate f on the unique 0-length vector, the existential statement ∃v, f(v) holds if and only if f([]) holds, since there is only one vector of length 0, namely the empty vector.

Русский

Для предиката f над единственным вектором нулевой длины существование вектора v с выполнением f(v) эквивалентно выполнению f([]), так как нулевой вектор единственный.

LaTeX

$$$(\exists v : Vector3(\alpha,0),\; f(v)) \iff f([]).$$$

Lean4

theorem exists_vector_zero (f : Vector3 α 0 → Prop) : Exists f ↔ f [] :=
  ⟨fun ⟨v, fv⟩ => by rw [← eq_nil v]; exact fv, fun f0 => ⟨[], f0⟩⟩

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