OAI/NumberTheory/DukePrimeDegree/Geometry/PrefixExchangeRegions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Injective open regions in the exchanged prefix chart

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.fullRectangleCoordinates line 19
  2. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.fullRectangleCoordinates_isOpenEmbedding line 24
  3. def OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleCoordinates line 30
  4. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleCoordinates_isOpenEmbedding line 34
  5. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleCoordinates_param line 40
  6. def OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleRegion line 49
  7. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleRegion_open line 53
  8. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.exchangedRectangleRegion_embedding line 60