angle₂₃₁_eq_zero — Mathlib

English

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

Русский

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

LaTeX

$$$Sbtw\; p_1\; p_2\; p_3 \Rightarrow \angle p_1 p_2 p_3 = \pi$$$

Lean4

/-- If the second of three points is strictly between the other two, the angle at the third 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_right

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