OAI/GroupTheory/PolycyclicRecognition/Analysis/ProbeTileSelector.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_measurable_probe_tile_index line 14

   Source documentation

   A measurable finite partition gives a measurable tile index on its covered set. Empty tiles and an empty covered set cause no difficulty.

   theorem exists_measurable_probe_tile_index
       {X : Type*} [MeasurableSpace X] {m : ℕ}
       (U : Set X) (tile : Fin m → Set X)
       (hm : ∀ j, MeasurableSet (tile j))
       (hd : Pairwise (fun j k => Disjoint (tile j) (tile k)))
       (hcover : (⋃ j, tile j) = U) :
       ∃ index : U → Fin m, Measurable index ∧
         (∀ x, x.val ∈ tile (index x)) ∧
         ∀ j, index ⁻¹' {j} = Subtype.val ⁻¹' tile j := by
   …