OAI/Combinatorics/CompleteCrossing/Tensor.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Geometric crossing tensors, local orders, supports, and bilinear chain pairings.

  1. theorem OAI.Paper170.interiorIntersection_swap line 19
  2. theorem OAI.Paper170.spokeComparison_swap line 34
  3. theorem OAI.Paper170.cycle_intersection_skew line 48
  4. theorem OAI.Paper170.edgePairing_neg_left line 64
  5. theorem OAI.Paper170.edgePairing_neg_right line 68
  6. theorem OAI.Paper170.edgePairing_swap line 72
  7. theorem OAI.Paper170.completeEdgeVector_self line 84
  8. theorem OAI.Paper170.completeEdgeVector_reverse line 91
  9. theorem OAI.Paper170.raw_cycle_symmetries line 103
  10. theorem OAI.Paper170.completeEdgeVector_endpoints line 137
  11. theorem OAI.Paper170.rawCycleIntersection_endpoints line 153
  12. theorem OAI.Paper170.independent_cycleIntersection line 159
  13. theorem OAI.Paper170.interiorIntersection_ne_zero_crossing line 179
  14. theorem OAI.Paper170.signed_support_bound line 205
  15. theorem OAI.Paper170.Graph.common_endpoint_unique line 243
  16. theorem OAI.Paper170.endpointSign_eq_zero line 252
  17. theorem OAI.Paper170.endpointSign_sq line 256
  18. theorem OAI.Paper170.adjacent_interiorIntersection_eq_zero line 262
  19. theorem OAI.Paper170.cycleIntersection_incident line 273
  20. def OAI.Paper170.completeIncidentEdge line 293
  21. theorem OAI.Paper170.completeIncidentEdge_neighbor line 298
  22. theorem OAI.Paper170.completeIncidentEdge_injective line 303
  23. theorem OAI.Paper170.completeEdgeVector_incident line 311
  24. theorem OAI.Paper170.edgePairing_smul_smul line 324
  25. theorem OAI.Paper170.halfOrder_self line 333
  26. theorem OAI.Paper170.complete_local_orders line 338
  27. theorem OAI.Paper170.boundary_sum line 394
  28. theorem OAI.Paper170.boundary_mul line 399
  29. theorem OAI.Paper170.edgePairing_sum_left line 403
  30. theorem OAI.Paper170.edgePairing_sum_right line 409
  31. theorem OAI.Paper170.edgePairing_mul_left line 415
  32. theorem OAI.Paper170.edgePairing_mul_right line 419
  33. theorem OAI.Paper170.boundary_completeEdgeVector line 429
  34. def OAI.Paper170.liftedChain line 450
  35. theorem OAI.Paper170.boundary_liftedChain line 454
  36. theorem OAI.Paper170.chainPairing_rawCycleIntersection line 462
  37. theorem OAI.Paper170.edgePairing_add_left line 492
  38. theorem OAI.Paper170.edgePairing_add_right line 496
  39. theorem OAI.Paper170.edgePairing_smul_left line 500
  40. theorem OAI.Paper170.edgePairing_smul_right line 504
  41. theorem OAI.Paper170.edgePairing_eq_zero_of_simple_cycles line 508
  42. theorem OAI.Paper170.SimpleCycle.cyclicDart_coe line 549
  43. theorem OAI.Paper170.SimpleCycle.edgeChain_eq_dart_sum line 552
  44. theorem OAI.Paper170.edgePairing_single_single line 567
  45. theorem OAI.Paper170.edgePairing_simple_cycles line 571
  46. theorem OAI.Paper170.edgePairing_simple_cycles_range line 583