oangle_eq_pi_iff_sbtw — Mathlib

English

The oriented angle equals π iff the second point lies strictly between the first and third, i.e., Sbtw ℝ p1 p2 p3.

Русский

Ориентированный угол равен π тогда, когда вторая точка лежит строго между первой и третьей, т.е. Sbtw ℝ p1 p2 p3.

LaTeX

$$$\measuredangle p_1 p_2 p_3 = \pi \iff Sbtw \mathbb{R}\, p_1\ p_2\ p_3$$$

Lean4

/-- The oriented angle between three points is π if and only if the second point is strictly
between the other two. -/
theorem oangle_eq_pi_iff_sbtw {p₁ p₂ p₃ : P} : ∡ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃ := by
  rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]

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