oangle₂₃₁_eq_zero — Mathlib

English

Let p1, p2, p3 be points with p2 weakly between p1 and p3. Then the oriented angle at p3 between p2 and p1 is zero: ∡ p2 p3 p1 = 0.

Русский

Пусть p1, p2, p3 — точки так, что p2 лежит на отрезке между p1 и p3 в слабом смысле. Тогда ориентированный угол ∡ p2 p3 p1 равен нулю: ∡ p2 p3 p1 = 0.

LaTeX

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

Lean4

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

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