OAI/Geometry/Cannon/PlaneTopology/Spans.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonEmbeddedArc.Arc.tame_incident_segment line 57
  2. lemma OAI.CannonEmbeddedArc.Arc.radial_mem_segment line 68
  3. theorem OAI.CannonEmbeddedArc.Arc.noncut_face_degree_two line 76
  4. lemma OAI.CannonEmbeddedArc.Arc.cycle_edge_otherpoint line 158
  5. theorem OAI.CannonEmbeddedArc.Arc.noncut_face_second_edge line 177
  6. def OAI.CannonEmbeddedArc.Arc.Spans line 245
  7. lemma OAI.CannonEmbeddedArc.Arc.Spans.symm line 247
  8. lemma OAI.CannonEmbeddedArc.Arc.Spans.mem_left line 251
  9. lemma OAI.CannonEmbeddedArc.Arc.Spans.mem_right line 255
  10. lemma OAI.CannonEmbeddedArc.Arc.Spans.ne line 256
  11. lemma OAI.CannonEmbeddedArc.Arc.Spans.vertex_left line 260
  12. lemma OAI.CannonEmbeddedArc.Arc.Spans.vertex_right line 262
  13. lemma OAI.CannonEmbeddedArc.Arc.Spans.other_unique line 264
  14. lemma OAI.CannonEmbeddedArc.Arc.spans_edge_unique line 270
  15. lemma OAI.CannonEmbeddedArc.Arc.vertex_spans line 275
  16. abbrev OAI.CannonEmbeddedArc.Arc.GraphVertices line 283
  17. instance OAI.CannonEmbeddedArc.Arc.graphVertices_finite line 284
  18. def OAI.CannonEmbeddedArc.Arc.edgeGraph line 286
  19. lemma OAI.CannonEmbeddedArc.Arc.face_edge_eq line 291
  20. theorem OAI.CannonEmbeddedArc.Arc.facial_graph_isCycles line 310
  21. def OAI.CannonEmbeddedArc.Arc.edgeStart line 343
  22. def OAI.CannonEmbeddedArc.Arc.edgeEnd line 344
  23. def OAI.CannonEmbeddedArc.Arc.edgeKey line 345
  24. lemma OAI.CannonEmbeddedArc.Arc.edgeKey_eq line 346
  25. lemma OAI.CannonEmbeddedArc.Arc.edgeKey_injective line 351
  26. def OAI.CannonEmbeddedArc.Arc.walkCarrier line 357
  27. lemma OAI.CannonEmbeddedArc.Arc.walkCarrier_cons line 360
  28. lemma OAI.CannonEmbeddedArc.Arc.walkCarrier_vertex line 376
  29. lemma OAI.CannonEmbeddedArc.Arc.oriented_arc line 386
  30. theorem OAI.CannonEmbeddedArc.Arc.simple_walk_arc line 392
  31. lemma OAI.CannonEmbeddedArc.Arc.walkCarrier_subset line 450
  32. lemma OAI.CannonEmbeddedArc.Arc.cycle_saturated line 455
  33. theorem OAI.CannonEmbeddedArc.Arc.simple_cycle_arcs line 465
  34. theorem OAI.CannonEmbeddedArc.Arc.cycle_edges_isolated line 503
  35. theorem OAI.CannonEmbeddedArc.Arc.pair_no_cut line 531
  36. theorem OAI.CannonEmbeddedArc.Arc.pair_component_local_access line 579