left_ne_zero_of_oangle_eq_pi_div_two

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

← MathLib Explorer

English

If o.oangle(x,y) ≠ 0, then x ≠ 0.

Русский

Если o.oangle(x,y) ≠ 0, то x ≠ 0.

LaTeX

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

Lean4

/-- If the angle between two vectors is `π / 2`, the first vector is nonzero. -/
theorem left_ne_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0)

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

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

Разделы

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

Аффилиация

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