oangle_eq_zero_or_eq_pi_iff_not_linearIndependent

English

If x,y,z are nonzero, the angle from x to z equals the sum of angles from x to y and from y to z: o.oangle x y + o.oangle y z = o.oangle x z.

Русский

Если векторы x,y,z не нулевые, то угол от x к z равен сумме углов от x к y и от y к z: o.oangle x y + o.oangle y z = o.oangle x z.

LaTeX

$$$o.oangle x y + o.oangle y z = o.oangle x z$$$

Lean4

/-- The oriented angle between two vectors is zero or `π` if and only if those two vectors are
not linearly independent. -/
theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} :
    o.oangle x y = 0 ∨ o.oangle x y = π ↔ ¬LinearIndependent ℝ ![x, y] := by
  rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
    sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]

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