English
The unoriented angle equals the absolute value of the oriented angle converted to a real: InnerProductGeometry.angle x y = |(o.oangle x y).toReal|.
Русский
Неориентированный угол равен модулю ориентированного угла, приведённому к действительному числу: ∠(x,y) = |(o.oangle x y).toReal|.
LaTeX
$$$ InnerProductGeometry.angle x y = \left| (o.oangle x y).toReal \right| $$$
Lean4
/-- The unoriented angle between two nonzero vectors is the absolute value of the oriented angle,
converted to a real. -/
theorem angle_eq_abs_oangle_toReal {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
InnerProductGeometry.angle x y = |(o.oangle x y).toReal| :=
by
have h0 := InnerProductGeometry.angle_nonneg x y
have hpi := InnerProductGeometry.angle_le_pi x y
rcases o.oangle_eq_angle_or_eq_neg_angle hx hy with (h | h)
· rw [h, eq_comm, Real.Angle.abs_toReal_coe_eq_self_iff]
exact ⟨h0, hpi⟩
· rw [h, eq_comm, Real.Angle.abs_toReal_neg_coe_eq_self_iff]
exact ⟨h0, hpi⟩
