oangle_eq_add_pi_left — Mathlib

English

Replacing the first point by a point on the same line but the opposite ray changes the angle by π only.

Русский

Замена первой точки на точку на противоположном луче меняет угол на π.

LaTeX

$$$\angle p_1 p_2 p_3 = \angle p_1 p_2 p_3' + \pi$$$

Lean4

/-- Replacing the first point by one on the same line but the opposite ray adds π to the oriented
angle. -/
theorem _root_.Sbtw.oangle_eq_add_pi_left {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_swap h.left_ne h.right_ne hp₃p₂]

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