angle₁₃₂_eq_zero_of_ne — Mathlib

English

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

Русский

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

LaTeX

$$$Wbtw\; p_1\; p_2\; p_3 \Rightarrow \angle p_3 p_1 p_2 = 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 (reversed) 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₃

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