OAI/Geometry/RCD/Metric/ConvexPackingGrid.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separated finite grids inside the convex hull of independent points

  1. def OAI.RegularPointCoordinates.convexGridPoint line 15
  2. theorem OAI.RegularPointCoordinates.convexGridPoint_mem line 18
  3. theorem OAI.RegularPointCoordinates.convexGridPoint_separated line 34