OAI/Geometry/Immersion/ClosedSurface/PhaseGrid.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClosedSurfaceR4.PhaseGrid.Index line 11
  2. abbrev OAI.ClosedSurfaceR4.PhaseGrid.Base line 12
  3. def OAI.ClosedSurfaceR4.PhaseGrid.cell line 14
  4. def OAI.ClosedSurfaceR4.PhaseGrid.color line 17
  5. lemma OAI.ClosedSurfaceR4.PhaseGrid.same_color_difference line 20
  6. lemma OAI.ClosedSurfaceR4.PhaseGrid.divided_ne_abs_ge line 25
  7. theorem OAI.ClosedSurfaceR4.PhaseGrid.same_color_disjoint line 37
  8. def OAI.ClosedSurfaceR4.PhaseGrid.quantize line 65
  9. lemma OAI.ClosedSurfaceR4.PhaseGrid.coordinate_floor_near line 68
  10. lemma OAI.ClosedSurfaceR4.PhaseGrid.quantize_covers line 80
  11. def OAI.ClosedSurfaceR4.PhaseGrid.box line 85
  12. lemma OAI.ClosedSurfaceR4.PhaseGrid.floor_mem_interval line 88
  13. lemma OAI.ClosedSurfaceR4.PhaseGrid.finite_box_covers line 104
  14. lemma OAI.ClosedSurfaceR4.PhaseGrid.box_card line 111
  15. lemma OAI.ClosedSurfaceR4.PhaseGrid.box_card_bound line 119