OAI/CategoryTheory/Thomason/TwoCellComparison.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Two Cell Comparison.

  1. lemma OAI.Thomason.OmegaCategory.join_six_exchange line 14
  2. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_left_match line 103
  3. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_right_match line 107
  4. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_left₂_match line 111
  5. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_right₂_match line 117
  6. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_lc line 123
  7. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_cr line 127
  8. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp line 130
  9. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_entry line 158
  10. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_exit line 162
  11. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.comp_value line 166
  12. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.seam_of_matching line 266
  13. lemma OAI.Thomason.OmegaCategory.join_comp_source line 294
  14. lemma OAI.Thomason.OmegaCategory.join_comp_target line 311
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_whisker_left line 340
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_whisker_right line 354
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_whisker_left line 364
  18. lemma OAI.Thomason.GrayRecursive.IntervalHom.whiskeredVertical_whisker_right line 378
  19. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.source_zero line 391
  20. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.target_zero line 397
  21. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whisker_left_match line 405
  22. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whisker_left_source_match line 409
  23. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whiskerLeft line 412
  24. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whiskerLeft_value line 431
  25. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whisker_right_match line 458
  26. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whisker_right_target_match line 462
  27. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whiskerRight line 465
  28. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.whiskerRight_value line 484
  29. def OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.map line 526
  30. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.map_entry line 543
  31. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.map_exit line 548
  32. lemma OAI.Thomason.GrayRecursive.IntervalHom.CrossingSquare.map_value line 553
  33. inductive OAI.Thomason.GrayRecursive.IntervalHom.SquareNormal line 574
  34. lemma OAI.Thomason.GrayRecursive.IntervalHom.SquareNormal.bounded line 579
  35. lemma OAI.Thomason.GrayRecursive.IntervalHom.SquareNormal.map line 585
  36. lemma OAI.Thomason.GrayRecursive.IntervalHom.globe_inv_square_normal line 593
  37. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_square_normal line 622
  38. lemma OAI.Thomason.GrayRecursive.IntervalHom.vertical_square_normal line 627
  39. lemma OAI.Thomason.GrayRecursive.IntervalHom.SquareNormal.join_zero line 633
  40. lemma OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal.square line 664
  41. lemma OAI.Thomason.GrayRecursive.IntervalHom.endpoint_crossing_square_not_matching line 686
  42. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossing_square_endpoint_not_matching line 701
  43. lemma OAI.Thomason.GrayRecursive.IntervalHom.SquareNormal.join_one line 716
  44. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_square_normal line 738
  45. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_twocells_injective line 752
  46. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_twocells_bijective line 767
  47. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_poset_twocells_bijective line 774