left_ne_zero_of_oangle_sign_ne_zero

English

If the sign of the angle is nonzero, the left vector is nonzero: (o.oangle x y).sign ≠ 0 ⇒ x ≠ 0.

Русский

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

LaTeX

$$$(o.oangle x y).\sign \neq 0 \Rightarrow x \neq 0$$$

Lean4

/-- If the sign of the angle between two vectors is nonzero, the first vector is nonzero. -/
theorem left_ne_zero_of_oangle_sign_ne_zero {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

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