oangle_eq_left_right — Mathlib

English

Replacing both the first and third points by points on opposite rays preserves the angle sign relation.

Русский

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

LaTeX

$$$\angle p_1 p_2 p_3\;\text{sign} = \angle p_1' p_2 p_3'\;\text{sign}$$$

Lean4

/-- Replacing both the first and third points by ones on the same lines but the opposite rays
does not change the oriented angle (vertically opposite angles). -/
theorem _root_.Sbtw.oangle_eq_left_right {p₁ p₁' p₂ p₃ p₃' : P} (h₁ : Sbtw ℝ p₁ p₂ p₁') (h₃ : Sbtw ℝ p₃ p₂ p₃') :
    ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃' := by
  rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
    Real.Angle.coe_pi_add_coe_pi, add_zero]

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