oangle_eq_add_pi_right — Mathlib

English

Replacing both first and third points with opposite rays does not change the sign of the oriented angle (vertical angles).

Русский

Замена как первой, так и третьей точки на противоположные лучи не изменяет знак ориентированного угла (вертикальные углы).

LaTeX

$$$\angle p_1 p_2 p_3 = \angle p_1' p_2 p_3'\;\text{(mod } \pi\text{)}$$$

Lean4

/-- Replacing the third point by one on the same line but the opposite ray adds π to the oriented
angle. -/
theorem _root_.Sbtw.oangle_eq_add_pi_right {p₁ p₂ p₃ p₃' : P} (h : Sbtw ℝ p₃ p₂ p₃') (hp₁p₂ : p₁ ≠ p₂) :
    ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + π := by rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]

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