OAI/Geometry/Cannon/PlanarGraphs/Support.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonPlanarEuler.support line 56
  2. def OAI.CannonPlanarEuler.vertices line 57
  3. def OAI.CannonPlanarEuler.faces line 60
  4. lemma OAI.CannonPlanarEuler.support_insert line 62
  5. lemma OAI.CannonPlanarEuler.vertices_insert line 65
  6. lemma OAI.CannonPlanarEuler.support_closed line 72
  7. lemma OAI.CannonPlanarEuler.mem_vertices line 75
  8. lemma OAI.CannonPlanarEuler.vertices_subset line 80
  9. lemma OAI.CannonPlanarEuler.support_subtype line 85
  10. lemma OAI.CannonPlanarEuler.support_tame line 88
  11. lemma OAI.CannonPlanarEuler.faces_finite line 94
  12. lemma OAI.CannonPlanarEuler.edge_interior_avoids line 103
  13. lemma OAI.CannonPlanarEuler.edge_end_mem_support line 114
  14. lemma OAI.CannonPlanarEuler.edge_face line 128
  15. lemma OAI.CannonPlanarEuler.single_arc_faces line 145
  16. lemma OAI.CannonPlanarEuler.attached_edge_euler line 165
  17. lemma OAI.CannonPlanarEuler.mem_support line 235
  18. lemma OAI.CannonPlanarEuler.support_mono line 238
  19. lemma OAI.CannonPlanarEuler.support_nonempty line 243
  20. lemma OAI.CannonPlanarEuler.exists_attached_edge line 247
  21. theorem OAI.CannonPlanarEuler.planar_euler line 267