cos_eq_one_iff_angle_eq_zero — Mathlib

English

cos(angle x y) = 1 iff angle x y = 0.

Русский

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

LaTeX

$$cos(angle x y) = 1 ↔ angle x y = 0$$

Lean4

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

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