cos_oangle_eq_cos_angle — Mathlib

English

For nonzero x,y, the cosine of the oriented angle equals the cosine of the unoriented angle: Real.Angle.cos(o.oangle x y) = Real.cos(InnerProductGeometry.angle x y).

Русский

Для ненулевых векторов x,y косинус ориентированного угла равен косинусу неориентированного угла: Real.Angle.cos(o.oangle x y) = Real.cos(InnerProductGeometry.angle x y).

LaTeX

$$$ x \neq 0 \land y \neq 0 \Rightarrow Real.Angle.cos(o.oangle x y) = Real.cos(InnerProductGeometry.angle x y) $$$

Lean4

/-- The cosine of the oriented angle between two nonzero vectors equals that of the unoriented
angle. -/
theorem cos_oangle_eq_cos_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.Angle.cos (o.oangle x y) = Real.cos (InnerProductGeometry.angle x y) := by
  rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]

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