eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero

English

If the sign of the oriented angle ∡ p1 p p2 is zero, then either p1 = p or p2 = p or the unoriented angle ∠ p1 p p2 is 0 or π.

Русский

Если знак ориентированного угла ∡ p1 p p2 равен нулю, то либо p1 = p, либо p2 = p, либо неориентированный угол ∠ p1 p p2 равен 0 или π.

LaTeX

$$$(\measuredangle p_1 p p_2).sign = 0 \Rightarrow (p_1 = p) \lor (p_2 = p) \lor (\angle p_1 p p_2 = 0) \lor (\angle p_1 p p_2 = \pi)$$$

Lean4

/-- If the sign of the oriented angle at `p` between two points is zero, either one of the points
equals `p` or the unoriented angle is 0 or π. -/
theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {p p₁ p₂ : P} (h : (∡ p₁ p p₂).sign = 0) :
    p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π := by
  convert o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h <;> simp

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