left_ne_zero_of_oangle_eq_pi — Mathlib

English

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

Русский

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

LaTeX

$$$o.oangle(x,y) = \pi \Rightarrow x \neq y$$$

Lean4

/-- If the angle between two vectors is `π`, the first vector is nonzero. -/
theorem left_ne_zero_of_oangle_eq_pi {x y : V} (h : o.oangle x y = π) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0)

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