English
If the two lines through pairs (p1,p2) and (p4,p5) are parallel and the lines through (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
$$$ (affineSpan Real (Set.insert p_1 (Set.singleton p_2))).Parallel (affineSpan Real (Set.insert p_4 (Set.singleton p_5))) \rightarrow\ (affineSpan Real (Set.insert p_3 (Set.singleton p_2))).Parallel (affineSpan Real (Set.insert p_6 (Set.singleton 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
/-- If corresponding pairs of points in two angles have the same vector span, twice those angles
are equal. -/
theorem two_zsmul_oangle_of_vectorSpan_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
(h₁₂₄₅ : vectorSpan ℝ ({ p₁, p₂ } : Set P) = vectorSpan ℝ ({ p₄, p₅ } : Set P))
(h₃₂₆₅ : vectorSpan ℝ ({ p₃, p₂ } : Set P) = vectorSpan ℝ ({ p₆, p₅ } : Set P)) :
(2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆ :=
by
simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅
exact o.two_zsmul_oangle_of_span_eq_of_span_eq h₁₂₄₅ h₃₂₆₅
