OAI/Geometry/PlaneColoring/MeasurableAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem160.exists_measurable_unit_distance_coloring_of_center_cover line 11

   Source documentation

   A countable cover admits a measurable least-index choice, so separated small cells give a measurable proper coloring, not merely an arbitrary one.

   theorem exists_measurable_unit_distance_coloring_of_center_cover
       {X I : Type*} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X]
       [Countable I] [Nonempty I] {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, Measurable c ∧
         ∀ x y : X, dist x y = 1 → c x ≠ c y := by
   …