left_ne_zero_of_oangle_sign_eq_neg_one

English

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

Русский

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

LaTeX

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

Lean4

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

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