oangle₃₁₂_eq_zero — Mathlib

English

If p1 lies between p3 and p2 in the order (p1,p2,p3), then the oriented angle ∡ p3 p2 p1 equals π.

Русский

Если p1 лежит между p3 и p2 по порядку (p1,p2,p3), то ∡ p3 p2 p1 = π.

LaTeX

$$$Sbtw\ Real p_1 p_2 p_3 \Rightarrow \measuredangle p_3 p_2 p_1 = \pi$$$

Lean4

/-- If the second of three points is weakly between the other two, the oriented angle at the
first point (reversed) is zero. -/
theorem _root_.Wbtw.oangle₃₁₂_eq_zero {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : ∡ p₃ p₁ p₂ = 0 := by
  rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_zero]

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