inner_rev_eq_zero_of_oangle_eq_pi_div_two

English

If the oriented angle equals −π/2, then the inner product between y and x is zero: ⟪y,x⟫ = 0.

Русский

Если ориентированный угол равен −π/2, то ⟪y,x⟫ = 0.

LaTeX

$$$ o.oangle x y = -\frac{\pi}{2} \Rightarrow ⟪y,x⟫ = 0 $$$

Lean4

/-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors
(reversed) is zero. -/
theorem inner_rev_eq_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : ⟪y, x⟫ = 0 := by
  rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two h]

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