English
If the lines determined by p1 p2 and p4 p5 are parallel and the lines p3 p2 and p6 p5 are parallel, then 2·∡ p1 p2 p3 = 2·∡ p4 p5 p6.
Русский
Если прямые через p1 p2 и через p4 p5 параллельны, и прямые через p3 p2 и p6 p5 параллельны, тогда 2·угол p1 p2 p3 равно 2·угол p4 p5 p6.
LaTeX
$$$ (AffineSubspace.affineSpan Real {p_1,p_2}) \parallel (AffineSubspace.affineSpan Real {p_4,p_5}) \rightarrow (AffineSubspace.affineSpan Real {p_3,p_2}) \parallel (AffineSubspace.affineSpan Real {p_6,p_5}) \rightarrow (2 : \mathbb{Z}) \!\cdot (\angle p_1 p_2 p_3) = (2 : \mathbb{Z}) \!\cdot (\angle p_4 p_5 p_6)$$$
Lean4
/-- Given three points not equal to `p`, adding the angles between them at `p` in cyclic order
results in 0. -/
theorem oangle_add_cyc3 {p p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) :
∡ p₁ p p₂ + ∡ p₂ p p₃ + ∡ p₃ p p₁ = 0 := by simp [*]
