sin_eq_one_iff_angle_eq_pi_div_two

English

sin(angle x y) = 1 iff angle x y = π/2.

Русский

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

LaTeX

$$sin(angle x y) = 1 ↔ angle x y = π/2$$

Lean4

/-- The sine of the angle between two vectors is 1 if and only if the angle is π / 2. -/
theorem sin_eq_one_iff_angle_eq_pi_div_two : sin (angle x y) = 1 ↔ angle x y = π / 2 :=
  by
  refine ⟨fun h => ?_, fun h => by rw [h, sin_pi_div_two]⟩
  rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, h]
  simp

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