OAI/Combinatorics/EuclideanRamsey/Spherical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanRamsey.ramsey_cospherical line 15

   Source documentation

   Every injective finite indexed Ramsey configuration is cospherical. This uses the existing Ramsey predicate, with arbitrary finite colorings and copies preserving the original pairwise distances. Empty configurations and singletons are included, and no ambient affine-span assumption is imposed.

   Distinct definitions of this name: ComparatorChallenges/EuclideanRamseySpherical.lean:19 (same statement text; different proof or body). Qualify references as OAI.EuclideanRamsey.ramsey_cospherical@path.

   theorem ramsey_cospherical {s d : ℕ} (a : Fin s → Space d)
       (ha : Function.Injective a) (hR : Ramsey a) :
       EuclideanGeometry.Cospherical (Set.range a) := by
   …

   Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Ramsey