oangle_eq_zero_iff_sameRay — Mathlib

English

The oriented angle between x and y is zero exactly when x and y lie on the same ray.

Русский

Ориентированный угол между x и y равен нулю тогда и только тогда, когда x и y лежат на одной луче.

LaTeX

$$$o.oangle x y = 0 \iff \text{SameRay}_{\mathbb{R}}(x,y)$$$

Lean4

/-- The oriented angle between two vectors is zero if and only if they are on the same ray. -/
theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y :=
  by
  rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
    Complex.arg_eq_zero_iff]
  simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y

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