OAI/MeasureTheory/FalconerCompletion/Measures/PathIndex2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.pathIndex line 18
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.pathIndex_lt line 22
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.pathIndex_div_leading line 29
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.pathIndex_injective line 36
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.exists_pathIndex line 58
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.pathIndex_take line 82
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell line 100
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurableSet_treeCell line 103
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_disjoint line 106
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_subset_take line 118
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_cover_root line 131