cos_eq_neg_one_iff_angle_eq_pi — Mathlib

English

cos(angle x y) = −1 iff angle x y = π.

Русский

cos(угол x y) = −1 тогда и только тогда, когда угол x y = π.

LaTeX

$$cos(angle x y) = -1 ↔ angle x y = π$$

Lean4

/-- The cosine of the angle between two vectors is -1 if and only if the angle is π. -/
theorem cos_eq_neg_one_iff_angle_eq_pi : cos (angle x y) = -1 ↔ angle x y = π :=
  by
  rw [← cos_pi]
  exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (right_mem_Icc.2 pi_pos.le)

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