ne_of_oangle_sign_eq_one — Mathlib

English

If the sign of the angle equals 1, then the vectors are not equal.

Русский

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

LaTeX

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

Lean4

/-- If the sign of the angle between two vectors is positive, the vectors are not equal. -/
theorem ne_of_oangle_sign_eq_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)

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