sub_mem_orthogonal_of_inner_left — Mathlib

English

If x-y has equal inner products with all elements of K, then x-y ∈ K⊥.

Русский

Если ⟪x−y, v⟫ одинаково для всех v ∈ K, то x−y ∈ K⊥.

LaTeX

$$$$ \forall v \in K, \langle x-y, v \rangle = 0 \Rightarrow x-y \in K^{\perp}. $$$$

Lean4

theorem sub_mem_orthogonal_of_inner_left {x y : E} (h : ∀ v : K, ⟪x, v⟫ = ⟪y, v⟫) : x - y ∈ Kᗮ :=
  by
  rw [mem_orthogonal']
  intro u hu
  rw [inner_sub_left, sub_eq_zero]
  exact h ⟨u, hu⟩

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