OAI/MeasureTheory/FalconerCompletion/Measures/AmbientGridCell3.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCell line 16
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mem_ambientGridCell_iff line 20
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.measurableSet_ambientGridCell line 25
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCell_disjoint line 37
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCell_dist_le line 45
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCell_subset_ancestor line 79
  7. def OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter line 94
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_apply line 97
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_mem line 100
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_injective line 109
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_coordinate_bound line 117
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_index_bounds line 131
  13. theorem OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_ball_card line 142
  14. theorem OAI.GraphLiteralSupport.Attempt4FullFar.translated_ambientGridCenter_ball_card line 168
  15. def OAI.GraphLiteralSupport.Attempt4FullFar.ambientAncestor line 179
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCenter_mem_ancestor line 182
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientAncestor_comp line 186
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientAncestor_coordinate line 194
  19. theorem OAI.GraphLiteralSupport.Attempt4FullFar.ambientAncestor_fiber_card line 203
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientAncestor_image_card line 225