angle₂₃₁_eq_zero_of_ne — Mathlib

English

If the second of three points is weakly between the other two, the angle at the third point (reversed) is zero.

Русский

Если вторая точка между двумя другими, угол в третьей точке равен нулю (обратно).

LaTeX

$$$Wbtw\; p_1\; p_2\; p_3 \Rightarrow \angle p_2 p_3 p_1 = 0$$$

Lean4

/-- If the second of three points is weakly between the other two, and not equal to the third,
the angle at the third point is zero. -/
theorem _root_.Wbtw.angle₂₃₁_eq_zero_of_ne {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₃ : p₂ ≠ p₃) : ∠ p₂ p₃ p₁ = 0 :=
  h.symm.angle₂₁₃_eq_zero_of_ne hp₂p₃

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