OAI/NumberTheory/DukePrimeDegree/Entropy/WholeFutureCountableCover.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A countable family of boxes containing complete future fibers

The family is chosen before the sample. Bounded future fibers, transported to the sampled coordinates, fit into one member of this fixed family. This is the countability needed for gluing the local future laws.

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.wholeFutureBoxFamily line 23
  2. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.wholeFutureBoxFamily_countable line 27
  3. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.exists_countable_box_containing_futureFiber line 33
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_exists_countable_wholeFuture_box line 78