ne_of_oangle_sign_ne_zero

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

URI: https://scilib.ai/kg/mathlib#Orientation.ne_of_oangle_sign_ne_zero

← MathLib Explorer

English

If the sign of the angle is nonzero, then x ≠ y.

Русский

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

LaTeX

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

Lean4

/-- If the sign of the angle between two vectors is nonzero, the vectors are not equal. -/
theorem ne_of_oangle_sign_ne_zero {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ y :=
  o.ne_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru