sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi

English

The sine of the angle is zero precisely when the angle is 0 or π.

Русский

Синус угла равен нулю тогда и только тогда, когда угол равен 0 или π.

LaTeX

$$$$ \sin(\angle p_1 p_2 p_3) = 0 \iff \angle p_1 p_2 p_3 = 0 \lor \angle p_1 p_2 p_3 = \pi. $$$$

Lean4

/-- The sine of the angle between three points is 0 if and only if the angle is 0 or π. -/
nonrec theorem sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi {p₁ p₂ p₃ : P} :
    Real.sin (∠ p₁ p₂ p₃) = 0 ↔ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π :=
  sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi

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