oangle₁₂₃_eq_pi — Mathlib

English

If B is strictly between A and C (Sbtw), then the oriented angle ∡ A B C equals π.

Русский

Если B строго между A и C (Sbtw), то ориентированный угол ∡ A B C равен π.

LaTeX

$$$Sbtw\ ℝ\ p_1 p_2 p_3 \Rightarrow \angle p_1 p_2 p_3 = \pi$$$

Lean4

/-- If the second of three points is strictly between the other two, the oriented angle at that
point is π. -/
theorem _root_.Sbtw.oangle₁₂₃_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∡ p₁ p₂ p₃ = π :=
  oangle_eq_pi_iff_sbtw.2 h

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