inner_eq_zero_of_left — Mathlib

English

If x has zero norm, then its inner product with any y is zero: ⟪x,y⟫ = 0 when ∥x∥ = 0.

Русский

Если ∥x∥ = 0, то скалярное произведение с любым y равно нулю: ⟪x,y⟫ = 0.

LaTeX

$$$\|x\| = 0 \Rightarrow \langle x,y\rangle = 0$$$

Lean4

theorem inner_eq_zero_of_left {x : E} (y : E) (h : ‖x‖ = 0) : ⟪x, y⟫_𝕜 = 0 :=
  by
  rw [← norm_eq_zero]
  refine le_antisymm ?_ (by positivity)
  exact norm_inner_le_norm _ _ |>.trans <| by simp [h]

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