ne_of_oangle_eq_pi — Mathlib

English

If the oriented angle equals −π/2, the two vectors are not equal: o.oangle(x,y) = -π/2 ⇒ x ≠ y.

Русский

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

LaTeX

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

Lean4

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

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