OAI/Combinatorics/EuclideanRamsey/CircleSpan.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanRamsey.CircleConsequence.circle_five_affineSpan line 9

   Source documentation

   Three actual distinct circle points already affinely span the plane. The inverse two-by-two determinant is written explicitly.

   theorem circle_five_affineSpan (a : Fin 5 → Space 2)
       (ha : Function.Injective a) (c : Space 2) (r : ℝ)
       (hc : ∀ i, dist (a i) c = r) : affineSpan ℝ (Set.range a) = ⊤ := by
   …

   Mentions: OAI.EuclideanRamsey.Space