cos_eq_one_iff_angle_eq_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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