English
If s is cospherical and p1, p2, p3 are points in s that are pairwise distinct, then the triple (p1, p2, p3) is affinely independent.
Русский
Если s кососферно, и p1, p2, p3 — точки в s, попарно различны, тогда тройка (p1, p2, p3) афинно независима.
LaTeX
$$$\text{Cospherical}(s)\wedge p_1,p_2,p_3\in s\wedge p_1\neq p_2\wedge p_1\neq p_3\wedge p_2\neq p_3\Rightarrow\mathrm{AffineIndependent}_{\mathbb{R}}(![p_1,p_2,p_3])$$$
Lean4
/-- Any three points in a cospherical set are affinely independent. -/
theorem affineIndependent_of_mem_of_ne {s : Set P} (hs : Cospherical s) {p₁ p₂ p₃ : P} (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s)
(h₃ : p₃ ∈ s) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) : AffineIndependent ℝ ![p₁, p₂, p₃] :=
by
refine hs.affineIndependent ?_ ?_
· simp [h₁, h₂, h₃, Set.insert_subset_iff]
· erw [Fin.cons_injective_iff, Fin.cons_injective_iff]
simp [h₁₂, h₁₃, h₂₃, Function.Injective, eq_iff_true_of_subsingleton]
