OAI/NumberTheory/DukePrimeDegree/Geometry/PhysicalWindowAtlas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Countable compact-covering atlases of physical product windows

  1. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.exists_countable_physical_windows line 19
  2. def OAI.DukePrimeDegree.RootPrefixCoordinates.physicalWindowFamily line 39
  3. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalWindowFamily_countable line 43
  4. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalWindowFamily_time line 48
  5. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalWindowFamily_covers line 55
  6. theorem OAI.DukePrimeDegree.PhysicalPrefixWindow.exists_next_time_bound line 68