OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingRootProductBoxes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Unconditional local product boxes at every ordered-root step

  1. instance OAI.DukePrimeDegree.positiveRootGeneratedGroup_secondCountable line 14
  2. instance OAI.DukePrimeDegree.initialRemainingErase_standardBorel line 19
  3. def OAI.DukePrimeDegree.RootPrefixCoordinates.factorTime line 34
  4. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.continuous_factorTime line 37
  5. def OAI.DukePrimeDegree.RootPrefixCoordinates.rectangleSlice line 42
  6. def OAI.DukePrimeDegree.RootPrefixCoordinates.rectangleTime line 45
  7. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.rectangleSlice_isOpenEmbedding line 48
  8. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.continuous_rectangleTime line 53
  9. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.rectangleSlice_orbit line 58
  10. theorem OAI.DukePrimeDegree.remainingRootBox_conditional_product line 68
  11. theorem OAI.DukePrimeDegree.exists_remainingRoot_product_box line 104