OAI/MeasureTheory/FalconerCompletion/Measures/AmbientGridCell.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.CurrentFalconer.ambientGridCell line 13
  2. lemma OAI.CurrentFalconer.mem_ambientGridCell_iff line 17
  3. lemma OAI.CurrentFalconer.measurableSet_ambientGridCell line 22
  4. lemma OAI.CurrentFalconer.ambientGridCell_disjoint line 34
  5. lemma OAI.CurrentFalconer.ambientGridCell_dist_le line 42
  6. lemma OAI.CurrentFalconer.ambientGridCell_subset_ancestor line 76
  7. def OAI.CurrentFalconer.ambientGridCenter line 91
  8. lemma OAI.CurrentFalconer.ambientGridCenter_apply line 94
  9. lemma OAI.CurrentFalconer.ambientGridCenter_mem line 97
  10. lemma OAI.CurrentFalconer.ambientGridCenter_injective line 106
  11. lemma OAI.CurrentFalconer.ambientGridCenter_coordinate_bound line 114
  12. lemma OAI.CurrentFalconer.ambientGridCenter_index_bounds line 128
  13. theorem OAI.CurrentFalconer.ambientGridCenter_ball_card line 139
  14. theorem OAI.CurrentFalconer.translated_ambientGridCenter_ball_card line 165