OAI/Geometry/Cannon/PlanarGraphs/Region.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonFaceIncidence.region line 36
  2. def OAI.CannonFaceIncidence.incident line 39
  3. lemma OAI.CannonFaceIncidence.region_subset line 43
  4. lemma OAI.CannonFaceIncidence.region_isOpen line 47
  5. lemma OAI.CannonFaceIncidence.label_on_connected line 60
  6. theorem OAI.CannonFaceIncidence.sector_incidence line 69
  7. theorem OAI.CannonFaceIncidence.incident_constant_on_preconnected line 105
  8. def OAI.CannonFaceIncidence.openBox line 126
  9. def OAI.CannonFaceIncidence.halfBox line 127
  10. lemma OAI.CannonFaceIncidence.openBox_eq_ball line 130
  11. lemma OAI.CannonFaceIncidence.halfBox_connected line 134
  12. lemma OAI.CannonFaceIncidence.halfBox_closure line 139
  13. theorem OAI.CannonFaceIncidence.flat_chart_incidence line 150