OAI/NumberTheory/DukePrimeDegree/Geometry/RootRectangleMeasures.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The included independent rectangles have the actual ambient measure

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.rectangleBasePoint line 16
  2. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.continuous_rectangleBasePoint line 20
  3. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.rectangle_includedFiberPoint line 25
  4. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.map_included_rectangle line 40