OAI/CategoryTheory/Thomason/EdgeComparison.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Edge Comparison.

  1. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossingProfile_bounded line 16
  2. lemma OAI.Thomason.DirectedComplex.CylinderTables.leftProfile_bounded line 24
  3. lemma OAI.Thomason.DirectedComplex.CylinderTables.rightProfile_bounded line 35
  4. lemma OAI.Thomason.DirectedComplex.CylinderTables.object_rows_equal line 46
  5. lemma OAI.Thomason.DirectedComplex.CylinderTables.vertical_object_face line 52
  6. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_edge_left_target line 67
  7. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_edge_right_source line 84
  8. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_edge_matching_left line 101
  9. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_edge_matching_right line 108
  10. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_edge_factor line 116
  11. def OAI.Thomason.GrayRecursive.IntervalHom.verticalObject line 170
  12. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalObject_bounded line 173
  13. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalObject_face line 181
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalObject_source line 191
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalObject_target line 195
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.verticalObject_natural line 199
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_verticalObject line 203
  18. lemma OAI.Thomason.GrayRecursive.IntervalHom.composite_bounded line 209
  19. def OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge line 214
  20. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_left_matching line 219
  21. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_right_matching line 226
  22. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_bounded line 235
  23. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossingEdge line 247
  24. def OAI.Thomason.GrayRecursive.IntervalHom.crossingEdgeLift line 257
  25. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdgeLift_bounded line 264
  26. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossingEdgeLift line 272
  27. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_edges_surjective line 283
  28. theorem OAI.Thomason.GlobeComplex.complexPositiveAcyclic line 307
  29. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_source line 324
  30. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossingEdge_target line 334
  31. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_map_endpoint line 343
  32. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_map_crossingEdge line 348
  33. inductive OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal line 356
  34. lemma OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal.bounded line 364
  35. lemma OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal.map line 370
  36. lemma OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal.face_zero line 384
  37. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_as_map line 401
  38. lemma OAI.Thomason.GrayRecursive.IntervalHom.globe_inv_edge_normal line 410
  39. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_edge_normal line 441
  40. lemma OAI.Thomason.GrayRecursive.IntervalHom.endpoint_source line 457
  41. lemma OAI.Thomason.GrayRecursive.IntervalHom.endpoint_target line 461
  42. lemma OAI.Thomason.GrayRecursive.IntervalHom.endpoint_join_crossing line 465
  43. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossing_join_endpoint line 482
  44. lemma OAI.Thomason.GrayRecursive.IntervalHom.EdgeNormal.join line 494
  45. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_one_faces_normal line 526
  46. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_edge_normal line 584
  47. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossing_edge_table_matching_left line 601
  48. lemma OAI.Thomason.GrayRecursive.IntervalHom.crossing_edge_table_matching_right line 606
  49. lemma OAI.Thomason.GrayRecursive.IntervalHom.table_join_zero_row_succ line 614
  50. lemma OAI.Thomason.GrayRecursive.IntervalHom.table_join_zero_row_zero line 621
  51. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossingEdge_row_succ line 627
  52. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossingEdge_row_zero line 644
  53. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_crossingEdge_injective line 653
  54. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_edges_injective line 692
  55. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_edges_bijective line 709
  56. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_poset_edges_bijective line 719