dotProduct_eq_iff — Mathlib

English

Let v and w be vectors in R^n. If the dot product v · u equals w · u for every u in R^n, then v = w. Conversely, if v = w then their dot products with any u are equal.

Русский

Пусть v и w — векторы в R^n. Если скалярное произведение v · u равно w · u для каждого u в R^n, то v = w. И наоборот, если v = w, то их скалярные произведения с любым u равны.

LaTeX

$$$\bigl(\forall u: n \to R,\ v \cdot u = w \cdot u\bigr) \iff v = w$$$

Lean4

theorem dotProduct_eq_iff {v w : n → R} : (∀ u, v ⬝ᵥ u = w ⬝ᵥ u) ↔ v = w :=
  ⟨fun h => dotProduct_eq v w h, fun h _ => h ▸ rfl⟩

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