OAI/Geometry/UnitDistances/Sweep.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.Sweep.Lower line 9
  2. def OAI.PlanarUnitDistances.Sweep.GapBand line 12
  3. lemma OAI.PlanarUnitDistances.Sweep.links_cover line 15
  4. lemma OAI.PlanarUnitDistances.Sweep.links_sound line 32
  5. lemma OAI.PlanarUnitDistances.Sweep.gaps_cover line 64
  6. lemma OAI.PlanarUnitDistances.Sweep.gaps_avoid line 68
  7. lemma OAI.PlanarUnitDistances.Sweep.links_endpoints line 73
  8. lemma OAI.PlanarUnitDistances.Sweep.gaps_endpoints line 93
  9. def OAI.PlanarUnitDistances.SweepRuns.Reach line 105
  10. lemma OAI.PlanarUnitDistances.SweepRuns.reach_self line 109
  11. lemma OAI.PlanarUnitDistances.SweepRuns.reach_extend_left line 114
  12. def OAI.PlanarUnitDistances.SweepRuns.starts line 127
  13. lemma OAI.PlanarUnitDistances.SweepRuns.mem_starts line 130
  14. lemma OAI.PlanarUnitDistances.SweepRuns.starts_zero line 134
  15. lemma OAI.PlanarUnitDistances.SweepRuns.starts_succ line 138
  16. def OAI.PlanarUnitDistances.SweepRuns.last line 144
  17. def OAI.PlanarUnitDistances.SweepRuns.runs line 147
  18. lemma OAI.PlanarUnitDistances.SweepRuns.mem_runs line 151
  19. lemma OAI.PlanarUnitDistances.SweepRuns.runs_cover line 161
  20. lemma OAI.PlanarUnitDistances.SweepRuns.runs_card line 183
  21. lemma OAI.PlanarUnitDistances.CircleCutting.continuous_graphPoint line 196
  22. lemma OAI.PlanarUnitDistances.CircleCutting.unit_graph_closed line 201
  23. lemma OAI.PlanarUnitDistances.CircleCutting.circle_open_avoids_abscissas line 222
  24. abbrev OAI.PlanarUnitDistances.CircleCutting.Gap line 238
  25. def OAI.PlanarUnitDistances.CircleCutting.region line 240
  26. lemma OAI.PlanarUnitDistances.CircleCutting.region_open line 243
  27. lemma OAI.PlanarUnitDistances.CircleCutting.slab_list_transport line 264
  28. lemma OAI.PlanarUnitDistances.CircleCutting.slab_gap_avoids line 295
  29. structure OAI.PlanarUnitDistances.CircleCutting.Arrangement line 319
  30. lemma OAI.PlanarUnitDistances.CircleCutting.arrangement_exists line 329
  31. def OAI.PlanarUnitDistances.CircleCutting.Arrangement.criticalAt line 356
  32. def OAI.PlanarUnitDistances.CircleCutting.Arrangement.G line 359
  33. def OAI.PlanarUnitDistances.CircleCutting.Arrangement.pieces line 361
  34. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.list_card_le line 363
  35. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.G_card_le line 371
  36. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.skeleton line 374
  37. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.critical_sum line 384
  38. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.pieces_card line 401
  39. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.piece_avoids line 426
  40. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.pieces_cover line 440
  41. lemma OAI.PlanarUnitDistances.CircleCutting.circleIntersections_mono line 465
  42. lemma OAI.PlanarUnitDistances.CircleCutting.eventAbscissas_mono line 475
  43. lemma OAI.PlanarUnitDistances.CircleCutting.eventAbscissas_card line 483
  44. def OAI.PlanarUnitDistances.CircleCutting.endpoints line 492
  45. def OAI.PlanarUnitDistances.CircleCutting.boundaries line 495
  46. abbrev OAI.PlanarUnitDistances.CircleCutting.RegionCode line 498
  47. def OAI.PlanarUnitDistances.CircleCutting.codeRegion line 500
  48. def OAI.PlanarUnitDistances.CircleCutting.candidateCodes line 503
  49. lemma OAI.PlanarUnitDistances.CircleCutting.candidateCodes_card line 506
  50. lemma OAI.PlanarUnitDistances.CircleCutting.span_description line 526
  51. lemma OAI.PlanarUnitDistances.CircleCutting.Arrangement.piece_description line 573
  52. lemma OAI.PlanarUnitDistances.CircleCutting.rotate_surjective line 608
  53. lemma OAI.PlanarUnitDistances.CircleCutting.mem_circleIntersections_iff line 619
  54. lemma OAI.PlanarUnitDistances.CircleCutting.good_rotated_position line 632