English
Let s be an affine subspace of P. If p1 and p2 belong to s and p3, p4 lie on opposite sides of s, then the oriented angles ∡p1 p4 p2 and ∡p1 p3 p2 have opposite signs.
Русский
Пусть s — аффиново подпространство. Если p1 и p2 принадлежат s, а p3 и p4 лежат на противоположных сторонах от s, то знаки углов ∡p1 p4 p2 и ∡p1 p3 p2 противоположны.
LaTeX
$$$(\angle p_1 p_4 p_2).\operatorname{sign} = - (\angle p_1 p_3 p_2).\operatorname{sign}$$$
Lean4
/-- Given two points in an affine subspace, the angles between those two points at two other
points on opposite sides of that subspace have opposite signs. -/
theorem _root_.AffineSubspace.SOppSide.oangle_sign_eq_neg {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s) (hp₃p₄ : s.SOppSide p₃ p₄) : (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign :=
by
have hp₁p₃ : p₁ ≠ p₃ := by rintro rfl; exact hp₃p₄.left_notMem hp₁
rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂, ←
oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
(sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
