OAI/Geometry/Cannon/PlaneTopology/SquareSide.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonRegularDisk.squareSide line 22
  2. def OAI.CannonRegularDisk.squareBoundary line 25
  3. lemma OAI.CannonRegularDisk.squareSide_closed line 27
  4. lemma OAI.CannonRegularDisk.squareBoundary_closed line 30
  5. lemma OAI.CannonRegularDisk.mem_squareBoundary line 33
  6. theorem OAI.CannonRegularDisk.square_boundary_map line 37
  7. theorem OAI.CannonRegularDisk.IsRegularDisk.fill_square line 68
  8. def OAI.CannonGrid.point line 99
  9. def OAI.CannonGrid.strip line 103
  10. lemma OAI.CannonGrid.strip_closed line 106
  11. lemma OAI.CannonGrid.strip_cover line 111
  12. def OAI.CannonGrid.coordinate line 127
  13. def OAI.CannonGrid.patch line 132
  14. lemma OAI.CannonGrid.strip_overlap line 135
  15. lemma OAI.CannonGrid.patch_agree line 144
  16. def OAI.CannonGrid.glue line 170
  17. lemma OAI.CannonGrid.glue_apply line 175
  18. def OAI.CannonGrid.parameter line 182
  19. lemma OAI.CannonGrid.parameter_coordinate line 188
  20. lemma OAI.CannonGrid.parameter_zero line 195
  21. lemma OAI.CannonGrid.parameter_one line 197
  22. lemma OAI.CannonGrid.subdivision_fine line 207
  23. lemma OAI.CannonGrid.point_zero line 228
  24. lemma OAI.CannonGrid.point_last line 229
  25. lemma OAI.CannonGrid.glue_zero_right line 232
  26. lemma OAI.CannonGrid.glue_one_right line 243
  27. lemma OAI.CannonGrid.glue_bottom line 258
  28. theorem OAI.CannonLoopApproximation.loop_approximation line 272
  29. theorem OAI.CannonRelease.boundary_uniform_loop_graph line 371