right_ne_zero_of_oangle_sign_eq_one

English

If (o.oangle x y).sign ≠ 0, then left and right vectors are nonzero respectively.

Русский

Если (o.oangle x y).sign ненулевой, то соответствующие левые/правые векторы ненулевые.

LaTeX

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

Lean4

/-- If the sign of the angle between two vectors is positive, the second vector is nonzero. -/
theorem right_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : y ≠ 0 :=
  o.right_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

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