English
If s is cospherical and p1, p2, p3 are three distinct points in s, then the triple ![p1,p2,p3] is affinely independent.
Русский
Если s кососферно и p1, p2, p3 — три различных точки в s, то тройка ![p1,p2,p3] аффинно независима.
LaTeX
$$$\text{Cospherical}(s)\Rightarrow\forall p_1,p_2,p_3\in s\,\big( p_1\neq p_2\land p_1\neq p_3\land p_2\neq p_3\Rightarrow\mathrm{AffineIndependent}_{\mathbb{R}}(![p_1,p_2,p_3])\big)$$$
Lean4
/-- The three points of a cospherical set are affinely independent. -/
theorem affineIndependent_of_ne {p₁ p₂ p₃ : P} (hs : Cospherical ({ p₁, p₂, p₃ } : Set P)) (h₁₂ : p₁ ≠ p₂)
(h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) : AffineIndependent ℝ ![p₁, p₂, p₃] :=
hs.affineIndependent_of_mem_of_ne (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
(Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) h₁₂ h₁₃ h₂₃
