oangle₃₁₂_eq_zero — Mathlib

English

If the second point is strictly between the first and third, then the oriented angle ∡ p3 p1 p2 is zero.

Русский

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

LaTeX

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

Lean4

/-- If the second of three points is strictly between the other two, the oriented angle at the
first point (reversed) 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

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