oangle_eq_pi_iff_angle_eq_pi — Mathlib

English

The oriented angle equals π if and only if the second point lies strictly between the other two.

Русский

Ориентированный угол равен π тогда, когда вторая точка лежит строго между двумя другими точками.

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 unoriented angle is `π`. -/
theorem oangle_eq_pi_iff_angle_eq_pi {p₁ p₂ p₃ : P} : ∡ p₁ p₂ p₃ = π ↔ ∠ p₁ p₂ p₃ = π :=
  o.oangle_eq_pi_iff_angle_eq_pi

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