OAI/Combinatorics/CompleteCrossing/CycleSpace.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Cycle-space spanning, flows, simple cycles, and oriented darts.

  1. def OAI.Paper170.SimpleCycle.next line 22
  2. theorem OAI.Paper170.SimpleCycle.follows_next line 25
  3. theorem OAI.Paper170.SimpleCycle.next_eq_finRotate line 29
  4. theorem OAI.Paper170.SimpleCycle.next_val line 35
  5. theorem OAI.Paper170.SimpleCycle.next_ne_self line 43
  6. theorem OAI.Paper170.SimpleCycle.next_next_ne_self line 50
  7. theorem OAI.Paper170.SimpleCycle.edge_injective line 57
  8. theorem OAI.Paper170.SimpleCycle.edgeChain_at_edge line 72
  9. theorem OAI.Paper170.SimpleCycle.edgeChain_at_edge_ne_zero line 78
  10. theorem OAI.Paper170.SimpleCycle.edgeChain_eq_zero_of_not_mem_range line 83
  11. theorem OAI.Paper170.SimpleCycle.edgeChain_support line 90
  12. theorem OAI.Paper170.SimpleCycle.signed_boundary_step line 97
  13. theorem OAI.Paper170.SimpleCycle.boundary_edgeChain line 108
  14. lemma OAI.Paper170.incoming_has_outgoing line 142
  15. abbrev OAI.Paper170.FlowVertex line 175
  16. lemma OAI.Paper170.flow_successor_exists line 178
  17. def OAI.Paper170.flowNext line 188
  18. def OAI.Paper170.flowEdge line 191
  19. lemma OAI.Paper170.flowEdge_spec line 195
  20. lemma OAI.Paper170.flowArc_irrefl line 201
  21. lemma OAI.Paper170.flowArc_not_reverse line 206
  22. lemma OAI.Paper170.exists_positive_period line 226
  23. structure OAI.Paper170Geometry.OrientedDart line 254
  24. def OAI.Paper170Geometry.OrientedDart.fst line 260
  25. def OAI.Paper170Geometry.OrientedDart.snd line 262
  26. def OAI.Paper170Geometry.OrientedDart.symm line 264
  27. theorem OAI.Paper170Geometry.OrientedDart.symm_fst line 266
  28. theorem OAI.Paper170Geometry.OrientedDart.symm_snd line 269
  29. theorem OAI.Paper170Geometry.OrientedDart.symm_symm line 272
  30. theorem OAI.Paper170Geometry.OrientedDart.fst_ne_snd line 275
  31. def OAI.Paper170Geometry.forwardDart line 284
  32. def OAI.Paper170Geometry.backwardDart line 286
  33. def OAI.Paper170Geometry.dartSign line 288
  34. theorem OAI.Paper170Geometry.orientedDart_cases line 290
  35. theorem OAI.Paper170Geometry.dart_source_incident line 298
  36. theorem OAI.Paper170Geometry.dart_target_incident line 306
  37. theorem OAI.Paper170Geometry.dartSign_symm line 314
  38. def OAI.Paper170.boundaryLinear line 330
  39. def OAI.Paper170.chainSupport line 339
  40. theorem OAI.Paper170.mem_chainSupport line 341
  41. theorem OAI.Paper170.simple_cycles_balanced line 344
  42. theorem OAI.Paper170.simple_cycles_span_of_supported_cycle line 354
  43. lemma OAI.Paper170.flow_period_three line 427
  44. theorem OAI.Paper170.exists_supported_simple_cycle line 454
  45. def OAI.Paper170.SimpleCycle.dart line 511
  46. theorem OAI.Paper170.SimpleCycle.dart_fst line 514
  47. theorem OAI.Paper170.SimpleCycle.dart_snd line 522
  48. theorem OAI.Paper170.SimpleCycle.dart_edge line 530
  49. theorem OAI.Paper170.SimpleCycle.dart_sign line 532
  50. def OAI.Paper170.SimpleCycle.modIndex line 536
  51. theorem OAI.Paper170.SimpleCycle.modIndex_succ line 539
  52. theorem OAI.Paper170.SimpleCycle.modIndex_period line 543
  53. def OAI.Paper170.SimpleCycle.cyclicDart line 547
  54. theorem OAI.Paper170.SimpleCycle.cyclicDart_seam line 549
  55. theorem OAI.Paper170.SimpleCycle.cyclicDart_period line 553
  56. theorem OAI.Paper170.SimpleCycle.cyclicDart_next_edge_ne line 556
  57. theorem OAI.Paper170.simple_cycles_span line 573