OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootWindows.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exhausting upper-root time by compactly contained cubes

The ordered real root coordinates give explicit increasing open cubes, compact closed cubes, and countable families of long quotient boxes.

  1. instance OAI.DukePrimeDegree.specialLinear_secondCountable line 20
  2. instance OAI.DukePrimeDegree.upperRootTransverse_secondCountable line 25
  3. def OAI.DukePrimeDegree.EliminationChain.cube line 32
  4. def OAI.DukePrimeDegree.EliminationChain.closedCube line 37
  5. lemma OAI.DukePrimeDegree.EliminationChain.cube_open line 42
  6. lemma OAI.DukePrimeDegree.EliminationChain.closedCube_compact line 47
  7. lemma OAI.DukePrimeDegree.EliminationChain.cube_subset_closedCube line 52
  8. lemma OAI.DukePrimeDegree.EliminationChain.cube_mono line 58
  9. lemma OAI.DukePrimeDegree.EliminationChain.mem_cube_exists line 65
  10. lemma OAI.DukePrimeDegree.EliminationChain.cubes_cover line 84
  11. def OAI.DukePrimeDegree.upperRootWindow line 92
  12. lemma OAI.DukePrimeDegree.upperRootWindow_open line 95
  13. lemma OAI.DukePrimeDegree.upperRootWindow_mono line 98
  14. lemma OAI.DukePrimeDegree.upperRootWindow_cover line 104
  15. lemma OAI.DukePrimeDegree.exists_countable_upperRootBoxes_exact_time line 107
  16. def OAI.DukePrimeDegree.upperRootLongBoxFamily line 128
  17. lemma OAI.DukePrimeDegree.upperRootLongBoxFamily_countable line 131
  18. lemma OAI.DukePrimeDegree.upperRootLongBoxFamily_time line 135
  19. lemma OAI.DukePrimeDegree.upperRootLongBoxFamily_covers line 140