OAI/Combinatorics/EuclideanRamsey/CircleExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanRamsey.CircleConsequence.stereographic line 10

   Source documentation

   Rational parametrization of a genuine radius-r circle.

   def stereographic (c : Space 2) (r t : ℝ) : Space 2 :=
   …

   Mentions: OAI.EuclideanRamsey.Space

2. theorem OAI.EuclideanRamsey.CircleConsequence.stereographic_recover line 13
3. theorem OAI.EuclideanRamsey.CircleConsequence.stereographic_injective line 20
4. theorem OAI.EuclideanRamsey.CircleConsequence.stereographic_on_circle line 40
5. theorem OAI.EuclideanRamsey.CircleConsequence.circle_infinite line 56
6. theorem OAI.EuclideanRamsey.CircleConsequence.extend_to_five line 63

   Source documentation

   Extension adds actual distinct points on the same metric circle.

   theorem extend_to_five {s : ℕ} (a : Fin s → Space 2)
       (hs : s ≤ 5) (ha : Function.Injective a)
       (c : Space 2) (r : ℝ) (hr : 0 < r)
       (hc : ∀ i, dist (a i) c = r) :
       ∃ b : Fin 5 → Space 2, Function.Injective b ∧
         (∀ j, dist (b j) c = r) ∧ ∃ f : Fin s → Fin 5, ∀ i, b (f i) = a i := by
   …

   Mentions: OAI.EuclideanRamsey.Space