ne_of_oangle_sign_eq_neg_one — Mathlib

English

If the sign of the oriented angle between x and y is -1, then x and y are not equal.

Русский

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

LaTeX

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

Lean4

/-- If the sign of the angle between two vectors is negative, the vectors are not equal. -/
theorem ne_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ y :=
  o.ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

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