cos_oangle_eq_cos_angle — Mathlib

English

Let p, p1, p2 be points with p1 ≠ p and p2 ≠ p. Then the cosine of the oriented angle ∡ p1 p p2 equals the cosine of the unoriented angle ∠ p1 p p2.

Русский

Пусть точки p, p1, p2 удовлетворяют p1 ≠ p и p2 ≠ p. Тогда косинус ориентированного угла ∡ p1 p p2 равен косинусу неориентированного угла ∠ p1 p p2.

LaTeX

$$$\cos\big(\measuredangle p_1 p p_2\big) = \cos\big(\angle p_1 p p_2\big)$$$

Lean4

/-- The cosine of the oriented angle at `p` between two points not equal to `p` equals that of the
unoriented angle. -/
theorem cos_oangle_eq_cos_angle {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) :
    Real.Angle.cos (∡ p₁ p p₂) = Real.cos (∠ p₁ p p₂) :=
  o.cos_oangle_eq_cos_angle (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

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