angle₃₁₂_eq_zero — Mathlib

English

If the second of three points is strictly between the other two, 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 strictly between the other two, the angle at the first point
(reversed) is zero. -/
theorem _root_.Sbtw.angle₃₁₂_eq_zero {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₃ p₁ p₂ = 0 :=
  h.wbtw.angle₃₁₂_eq_zero_of_ne h.ne_left

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