ne_of_oangle_eq_pi_div_two — Mathlib

English

If the oriented angle equals π or π/2 or −π/2, various nonzero conditions hold for the vectors involved.

Русский

Если угол равен π, π/2 или −π/2, для участвующих векторов выполняются различные ненулевые условия.

LaTeX

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

Lean4

/-- If the angle between two vectors is `π / 2`, the vectors are not equal. -/
theorem ne_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : x ≠ y :=
  o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0)

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