ext_inner_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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