oangle₁₃₂_eq_zero — Mathlib

English

If p2 lies weakly between p1 and p3 in the order p1, p2, p3, then the reversed oriented angle at p2 vanishes: ∡ p1 p3 p2 = 0.

Русский

Если p2 лежит между p1 и p3 в порядке p1, p2, p3, то обратный ориентированный угол ∡ p1 p3 p2 равен нулю.

LaTeX

$$$Wbtw_\mathbb{R}(p_1,p_2,p_3) \Rightarrow \angle p_1 p_3 p_2 = 0$$$

Lean4

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

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