cos_eq_zero_iff_angle_eq_pi_div_two

English

cos(angle x y) = 0 iff angle x y = π/2.

Русский

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

LaTeX

$$cos(angle x y) = 0 ↔ angle x y = π/2$$

Lean4

/-- The cosine of the angle between two vectors is 0 if and only if the angle is π / 2. -/
theorem cos_eq_zero_iff_angle_eq_pi_div_two : cos (angle x y) = 0 ↔ angle x y = π / 2 :=
  by
  rw [← cos_pi_div_two]
  apply injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩
  constructor <;> linarith [pi_pos]

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