oangle_eq_zero_iff_angle_eq_zero — Mathlib

English

The oriented angle equals π if and only if the unoriented angle equals π.

Русский

Ориентированный угол равен π тогда и только тогда, когда неориентированный угол равен π.

LaTeX

$$$\measuredangle p_1 p_2 p_3 = \pi \iff \angle p_1 p_2 p_3 = \pi$$$

Lean4

/-- The unoriented angle at `p` between two points not equal to `p` is zero if and only if the
unoriented angle is zero. -/
theorem oangle_eq_zero_iff_angle_eq_zero {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : ∡ p₁ p p₂ = 0 ↔ ∠ p₁ p p₂ = 0 :=
  o.oangle_eq_zero_iff_angle_eq_zero (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

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