OAI/NumberTheory/JointDickman/Arithmetic/OrderedPrimeBoundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Ordered prime tuples are continuity sets

  1. theorem OAI.JointDickman.strictMono_isOpen line 11
  2. theorem OAI.JointDickman.strictMono_frontier_subset line 33
  3. theorem OAI.JointDickman.orderedPrimeRegion_null_frontier line 43
  4. def OAI.JointDickman.orderedPrimeBox line 48
  5. theorem OAI.JointDickman.orderedPrimeBox_null_frontier line 51
  6. theorem OAI.JointDickman.orderedPrimeBox_measure_continuous line 57