inner_vsub_left_eq_zero_symm — Mathlib

English

For affine spaces, the inner product with a difference of points a -ᵥ b and a -ᵥ c is zero if and only if the inner product with b -ᵥ a and a -ᵥ c is zero.

Русский

Для аффинного пространства скалярное произведение с векторной разностью a -ᵥ b и a -ᵥ c равно нулю тогда и только тогда, когда скалярное произведение с b -ᵥ a и a -ᵥ c равно нулю.

LaTeX

$$$\langle a -ᵥ b, a -ᵥ c \rangle = 0 \iff \langle b -ᵥ a, a -ᵥ c \rangle = 0$$$

Lean4

theorem inner_vsub_left_eq_zero_symm {a b : P} {v : V} : ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0 := by
  rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]

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