angle₂₁₃_eq_zero — Mathlib

English

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

Русский

Если вторая из трёх точек лежит строго между двумя другими, угол в первой точке (обратно) равен 0.

LaTeX

$$$Sbtw\; 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
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

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