OAI/CategoryTheory/Thomason/PastingInterchange.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Pasting Interchange.

  1. abbrev OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.left line 23
  2. abbrev OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.right line 24
  3. abbrev OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.before line 25
  4. abbrev OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.suffix line 26
  5. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.midRight line 28
  6. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.A line 32
  7. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.B line 33
  8. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.C line 34
  9. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.B' line 35
  10. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.C' line 36
  11. def OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.Z line 37
  12. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.B_eq line 39
  13. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.C_eq line 55
  14. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.B'_eq line 72
  15. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.C'_eq line 87
  16. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.A_eq line 101
  17. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.Z_eq line 117
  18. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.AB line 132
  19. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.BC line 136
  20. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.CZ line 139
  21. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.AB' line 143
  22. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.BC' line 147
  23. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.CZ' line 150
  24. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.left_one_map line 154
  25. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.left_two_map line 170
  26. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.right_one_map line 187
  27. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.MixedZero.right_two_map line 201
  28. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_horizontal line 217
  29. lemma OAI.Thomason.GrayRecursive.concatInterval_horizontal line 268
  30. lemma OAI.Thomason.GrayRecursive.concatInterval_paste_zero line 292
  31. abbrev OAI.Thomason.GrayRecursive.MixedPositive.A line 319
  32. abbrev OAI.Thomason.GrayRecursive.MixedPositive.B line 320
  33. abbrev OAI.Thomason.GrayRecursive.MixedPositive.C line 321
  34. abbrev OAI.Thomason.GrayRecursive.MixedPositive.Z line 323
  35. lemma OAI.Thomason.GrayRecursive.MixedPositive.AC line 326
  36. lemma OAI.Thomason.GrayRecursive.MixedPositive.BZ line 331
  37. lemma OAI.Thomason.GrayRecursive.MixedPositive.AB line 336
  38. lemma OAI.Thomason.GrayRecursive.MixedPositive.C_map line 340
  39. lemma OAI.Thomason.GrayRecursive.MixedPositive.Z_map line 348
  40. lemma OAI.Thomason.GrayRecursive.MixedPositive.CZ line 356
  41. lemma OAI.Thomason.GrayRecursive.MixedPositive.left_one_map line 361
  42. lemma OAI.Thomason.GrayRecursive.MixedPositive.left_two_map line 379
  43. lemma OAI.Thomason.GrayRecursive.concatInterval_paste line 398
  44. lemma OAI.Thomason.GrayRecursive.FaceMatching.of_val line 469
  45. lemma OAI.Thomason.GrayRecursive.pasteCylinder_homCompose_stationary_right line 480
  46. lemma OAI.Thomason.GrayRecursive.pasteCylinder_homCompose_stationary_left line 493
  47. lemma OAI.Thomason.GrayRecursive.globeComposite_endpoint_val line 506
  48. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.D line 526
  49. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.E line 527
  50. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.S line 528
  51. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.T line 529
  52. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.suffix line 531
  53. def OAI.Thomason.GrayRecursive.ZeroInterchange.suffix' line 533
  54. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.suffix_matching line 539
  55. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.before line 550
  56. def OAI.Thomason.GrayRecursive.ZeroInterchange.before' line 552
  57. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.before_matching line 557
  58. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.A line 568
  59. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.C line 569
  60. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.B line 570
  61. abbrev OAI.Thomason.GrayRecursive.ZeroInterchange.Z line 571
  62. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.AC line 573
  63. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.BZ line 577
  64. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.AB line 581
  65. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.CZ line 585
  66. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.paste_one_map line 589
  67. lemma OAI.Thomason.GrayRecursive.ZeroInterchange.paste_two_map line 609
  68. lemma OAI.Thomason.GrayRecursive.pasteCylinder_interchange_zero line 632