OAI/Geometry/RCD/Metric/ProductPackingGrid.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A finite packing obtained from an extra metric direction

  1. theorem OAI.RegularPointCoordinates.metric_product_distance_L2 line 12
  2. def OAI.RegularPointCoordinates.productPackingGrid line 18
  3. theorem OAI.RegularPointCoordinates.productPackingGrid_separated line 22
  4. theorem OAI.RegularPointCoordinates.productPackingGrid_bounded line 35
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.product_grid_obstruction line 52