right_ne_zero_of_oangle_sign_eq_neg_one

English

If the sign of the oriented angle from x to y is -1, then y is nonzero.

Русский

Пусть o — ориентирование на двумерном вещественном пространстве V. Если знак ориентированного угла oangle(x, y) равен -1, то y ≠ 0.

LaTeX

$$$(o.oangle\;x\;y).\operatorname{sign} = -1 \Rightarrow y \neq 0$$$

Lean4

/-- If the sign of the angle between two vectors is negative, the second vector is nonzero. -/
theorem right_ne_zero_of_oangle_sign_eq_neg_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)

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