sub_mem_orthogonal_of_inner_right

English

If x and y have the same inner products with all v ∈ K on the right, then x−y ∈ K⊥.

Русский

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

LaTeX

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

Lean4

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

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