ext_inner_right — Mathlib

English

If two vectors have identical inner products with every first vector, then the vectors are equal.

Русский

Если два вектора имеют одинаковые скалярные произведения с любым первым вектором, то векторы равны.

LaTeX

$$$\forall v,\; \langle x, v\rangle = \langle y, v\rangle \;\Rightarrow\; x = y$$$

Lean4

theorem ext_inner_right {x y : E} (h : ∀ v, ⟪x, v⟫ = ⟪y, v⟫) : x = y := by
  rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]

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