English
If the vector spans of corresponding pairs match, then twice the oangle of the first triple equals twice the oangle of the second triple.
Русский
Если вектораSpan соответствующих пар совпадают, то дважды угол первого тройного набора равен удвоенному углу второго набора.
LaTeX
$$$\forall p_1,p_2,p_3,p_4,p_5,p_6:\ P,\ (vectorSpan\mathbb{R}({p_1,p_2}) = vectorSpan\mathbb{R}({p_4,p_5})) \land (vectorSpan\mathbb{R}({p_3,p_2}) = vectorSpan\mathbb{R}({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
/-- If twice the oriented angles between two triples of points are equal, one triple is affinely
independent if and only if the other is. -/
theorem affineIndependent_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
(h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆] := by
simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]
