oangle₂₃₁_eq_zero — Mathlib

English

If p2 strictly lies between p1 and p3, then the oriented angle at p3 between p2 and p1 is zero: ∡ p2 p3 p1 = 0.

Русский

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

LaTeX

$$$Sbtw_\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 strictly between the other two, the oriented angle at the
third point is zero. -/
theorem _root_.Sbtw.oangle₂₃₁_eq_zero {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∡ p₂ p₃ p₁ = 0 :=
  h.wbtw.oangle₂₃₁_eq_zero

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