oangle₂₁₃_eq_zero — Mathlib

English

Duplicate instance: if B is between A and C (Wbtw), then ∡ B A C = 0.

Русский

Дубликат: если B между A и C (Wbtw), то ∡ B A C = 0.

LaTeX

$$$Wbtw\ Real p_1 p_2 p_3 \Rightarrow \angle p_2 p_1 p_3 = 0$$$

Lean4

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

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