OAI/Combinatorics/EuclideanRamsey/Circle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanRamsey.CircleConsequence.five_circle_points_ramsey line 12

   Source documentation

   Every five-point subset of a circle is Ramsey.

   theorem five_circle_points_ramsey (a : Fin 5 → Space 2)
       (ha : Function.Injective a) (c : Space 2) (r : ℝ)
       (hc : ∀ i, dist (a i) c = r) : Ramsey a := by
   …

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

2. theorem OAI.EuclideanRamsey.CircleConsequence.at_most_five_circle_points_ramsey line 21

   Source documentation

   Every nonempty set of at most five distinct circle points is Ramsey, including singletons and zero-radius circles.

   Distinct definitions of this name: ComparatorChallenges/EuclideanRamseyCircle.lean:21 (same statement text; different proof or body). Qualify references as OAI.EuclideanRamsey.CircleConsequence.at_most_five_circle_points_ramsey@path.

   theorem at_most_five_circle_points_ramsey {s : ℕ} (a : Fin s → Space 2)
       (hs : 0 < s) (hs5 : s ≤ 5) (ha : Function.Injective a)
       (hsphere : ∃ c : Space 2, ∃ r : ℝ, ∀ i, dist (a i) c = r) : Ramsey a := by
   …

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