OAI/Geometry/PlaneColoring/Assembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem160.exists_unit_distance_coloring_of_center_cover line 12

   Source documentation

   A covering by small cells, whose equally colored distinct centers are far apart, gives a proper coloring of the unit-distance graph. The covering need not form a partition: classical choice assigns boundary points to one cell.

   theorem exists_unit_distance_coloring_of_center_cover
       {X I : Type*} [PseudoMetricSpace X] {k : ℕ}
       (center : I → X) (color : I → Fin k) (r : ℝ)
       (hcover : ∀ x : X, ∃ i : I, dist x (center i) ≤ r)
       (hdiam : 2 * r < 1)
       (hsep : ∀ i j : I, i ≠ j → color i = color j →
         1 + 2 * r < dist (center i) (center j)) :
       ∃ c : X → Fin k, ∀ x y : X, dist x y = 1 → c x ≠ c y := by
   …