oangle_ne_zero_and_ne_pi_iff_linearIndependent

English

The angle is 0 or π iff the second vector lies on the line generated by the first, or the first is zero.

Русский

Угол равен 0 или π тогда и только тогда, когда y лежит на линии, порождённой x, или x = 0.

LaTeX

$$$o.oangle x y = 0 \lor o.oangle x y = \pi \iff x = 0 \lor \exists r\in\mathbb{R},\ y = r\,x$$$

Lean4

/-- The oriented angle between two vectors is not zero or `π` if and only if those two vectors
are linearly independent. -/
theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} :
    o.oangle x y ≠ 0 ∧ o.oangle x y ≠ π ↔ LinearIndependent ℝ ![x, y] := by
  rw [← not_or, ← not_iff_not, Classical.not_not, oangle_eq_zero_or_eq_pi_iff_not_linearIndependent]

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