OAI/CategoryTheory/Thomason/StandardComparison.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Standard Comparison.

  1. lemma OAI.Thomason.GrayRecursive.table_functor_ext line 16
  2. def OAI.Thomason.GrayRecursive.tableCylinder line 59
  3. lemma OAI.Thomason.GrayRecursive.tableCylinder_endpoint line 62
  4. lemma OAI.Thomason.GrayRecursive.tableCylinder_endpoint_top line 67
  5. lemma OAI.Thomason.GrayRecursive.tableCylinder_vertical line 71
  6. lemma OAI.Thomason.GrayRecursive.tableCylinder_restrict line 75
  7. lemma OAI.Thomason.GrayRecursive.tableCylinder_matching line 89
  8. lemma OAI.Thomason.GrayRecursive.vertical_top_row line 99
  9. lemma OAI.Thomason.GrayRecursive.table_comp_bounded line 108
  10. lemma OAI.Thomason.GrayRecursive.restrictCylinder_vertical_top line 118
  11. lemma OAI.Thomason.GrayRecursive.tableCylinder_comp line 125
  12. def OAI.Thomason.GrayRecursive.IntervalHom.tableCell line 182
  13. lemma OAI.Thomason.GrayRecursive.IntervalHom.tableCell_of_bounded line 185
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.tableCell_face line 194
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.tableCell_comp line 200
  16. def OAI.Thomason.GrayRecursive.IntervalHom.chainDiagram line 215
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.tableCylinder_map line 221
  18. lemma OAI.Thomason.GrayRecursive.IntervalHom.tableCell_map line 232
  19. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainDiagram_natural line 240
  20. def OAI.Thomason.GrayRecursive.IntervalHom.chainComparison line 244
  21. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_generator line 247
  22. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_natural line 252
  23. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_endpoint line 261
  24. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_projection line 271
  25. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_globe line 281
  26. instance OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_globe_isIso line 296
  27. def OAI.Thomason.GrayRecursive.IntervalHom.intervalExtensionOfSimplexIsIso line 310
  28. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_simplexComparison_isIso line 330
  29. def OAI.Thomason.DirectedComplex.cylinderFunctor line 345
  30. def OAI.Thomason.NormalizedChains.complexOrderIso line 362
  31. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_isIso_of_iso line 394
  32. instance OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_empty_isIso line 407
  33. def OAI.Thomason.raisedOrientalChain line 428
  34. lemma OAI.Thomason.raisedOrientalChain_nu line 435
  35. lemma OAI.Thomason.raisedOrientalChain_of_nu line 452
  36. lemma OAI.Thomason.raisedOriental_nu_injective line 464
  37. lemma OAI.Thomason.NormalizedChains.table_truncated_of_card_le line 479
  38. lemma OAI.Thomason.NormalizedChains.edgeTable_bounded line 487
  39. def OAI.Thomason.GlobeComplex.topOneArrow line 508
  40. def OAI.Thomason.GlobeComplex.simplexOneFunctor line 513
  41. lemma OAI.Thomason.GlobeComplex.simplexOneFunctor_edge line 517
  42. lemma OAI.Thomason.GlobeComplex.simplexOneFunctor_vertex line 526
  43. def OAI.Thomason.GlobeComplex.toSimplexOne line 536
  44. def OAI.Thomason.GlobeComplex.fromSimplexOne line 540
  45. lemma OAI.Thomason.GlobeComplex.toSimplexOne_top line 545
  46. lemma OAI.Thomason.GlobeComplex.fromSimplexOne_edge line 549
  47. lemma OAI.Thomason.GlobeComplex.to_fromSimplexOne line 556
  48. lemma OAI.Thomason.GlobeComplex.fromSimplexOne_vertex line 561
  49. lemma OAI.Thomason.GlobeComplex.toSimplexOne_face line 569
  50. lemma OAI.Thomason.GlobeComplex.from_toSimplexOne line 578
  51. def OAI.Thomason.GlobeComplex.simplexOneIso line 604
  52. def OAI.Thomason.GlobeComplex.toSimplexZero line 621
  53. def OAI.Thomason.GlobeComplex.fromSimplexZero line 625
  54. lemma OAI.Thomason.GlobeComplex.fromSimplexZero_nu line 629
  55. lemma OAI.Thomason.GlobeComplex.toSimplexZero_top line 635
  56. lemma OAI.Thomason.GlobeComplex.simplexZero_table_unique line 640
  57. lemma OAI.Thomason.GlobeComplex.to_fromSimplexZero line 653
  58. lemma OAI.Thomason.GlobeComplex.from_toSimplexZero line 658
  59. def OAI.Thomason.GlobeComplex.simplexZeroIso line 666
  60. instance OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_simplexZero_isIso line 683
  61. instance OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_simplexOne_isIso line 687
  62. def OAI.Thomason.NormalizedChains.complexFinIso line 702
  63. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_small_isIso line 718
  64. lemma OAI.Thomason.GrayRecursive.IntervalHom.simplexComparison_isIso_of_standard line 728
  65. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standardSimplexComparison_isIso line 740
  66. lemma OAI.Thomason.OmegaCategory.Presentation.cells_induction line 754