OAI/CategoryTheory/Thomason/TwoCellExchange.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Two Cell Exchange.

  1. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_source_one line 17
  2. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_target_one line 28
  3. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_bounded_two line 40
  4. structure OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare line 53
  5. abbrev OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.entry line 67
  6. abbrev OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.exit line 68
  7. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.left₂_source_zero line 70
  8. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.left₂_target_zero line 76
  9. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.right₂_source_zero line 82
  10. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.right₂_target_zero line 88
  11. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle line 94
  12. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.first line 99
  13. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.last line 101
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.vertical_source_zero line 103
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.vertical_target_zero line 117
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle_matching_left line 131
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle_matching_right line 136
  18. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle_source line 144
  19. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle_target line 166
  20. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.first_source line 186
  21. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.first_target line 190
  22. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.last_source line 195
  23. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.last_target line 200
  24. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.first_middle line 205
  25. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.middle_last line 208
  26. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.firstMiddle_last line 211
  27. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.value line 216
  28. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.source_one line 219
  29. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.target_one line 224
  30. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.bounded line 228
  31. lemma OAI.Thomason.GrayRecursive.IntervalHom.table_join_row_above line 257
  32. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_middle line 268
  33. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_first line 277
  34. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_last line 281
  35. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_two line 285
  36. theorem OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_ext line 322
  37. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.ofTable line 391
  38. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.image_ofTable line 438
  39. theorem OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.unique_ofTable line 452
  40. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_comp_right line 473
  41. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_comp_left line 488
  42. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_middle line 509
  43. def OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical line 526
  44. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_left_match line 531
  45. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_right_match line 537
  46. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_source line 545
  47. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_target line 561
  48. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_one_source line 577
  49. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalCell_one_target line 583
  50. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_comp line 588
  51. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_exchange_right line 659
  52. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_exchange_left line 694