right_ne_zero_of_oangle_eq_neg_pi_div_two

English

If o.oangle(x,y) = π/2, then y ≠ 0.

Русский

Если угол равен π/2, второй вектор не нулевой.

LaTeX

$$$o.oangle(x,y) = \frac{\pi}{2} \Rightarrow y \neq 0$$$

Lean4

/-- If the angle between two vectors is `-π / 2`, the second vector is nonzero. -/
theorem right_ne_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : y ≠ 0 :=
  o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0)

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