cos_eq_neg_one_iff_angle_eq_pi — Mathlib

English

The cosine of the angle between two vectors equals -1 if and only if the angle is π.

Русский

Косинус угла между двумя векторами равен -1 тогда и только тогда, когда угол равен π.

LaTeX

$$$$ \cos(\angle x,y) = -1 \iff \angle x,y = \pi. $$$$

Lean4

/-- The cosine of the angle between three points is -1 if and only if the angle is π. -/
nonrec theorem cos_eq_neg_one_iff_angle_eq_pi {p₁ p₂ p₃ : P} : Real.cos (∠ p₁ p₂ p₃) = -1 ↔ ∠ p₁ p₂ p₃ = π :=
  cos_eq_neg_one_iff_angle_eq_pi

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