OAI/CategoryTheory/Thomason/SubdivisionPairing.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Subdivision Pairing.

  1. lemma OAI.Thomason.Subdivision.chainLast_singletonChain line 16
  2. lemma OAI.Thomason.Subdivision.chainLast_chainUnionMap line 20
  3. lemma OAI.Thomason.Subdivision.mem_initialFlag line 37
  4. def OAI.Thomason.Subdivision.collapseVertices line 42
  5. lemma OAI.Thomason.Subdivision.collapseVertices_apply line 46
  6. lemma OAI.Thomason.Subdivision.face_collapse_le line 49
  7. lemma OAI.Thomason.Subdivision.extraVertexFace_last line 57
  8. lemma OAI.Thomason.Subdivision.chainLast_extraVertex line 68
  9. lemma OAI.Thomason.Subdivision.extraVertex_initialFlag line 72
  10. lemma OAI.Thomason.Subdivision.extraVertex_eq_initialFlag_of_last_inserted line 88
  11. lemma OAI.Thomason.Subdivision.predAbove_le_eq_of_castSucc_lt line 105
  12. lemma OAI.Thomason.Subdivision.extraVertex_partialLastVertex line 121
  13. lemma OAI.Thomason.Subdivision.extraVertexMap_partialLastMap line 156
  14. lemma OAI.Thomason.Subdivision.exPairSimplex_level_iff line 167
  15. lemma OAI.Thomason.Subdivision.map_singletonChain line 181
  16. lemma OAI.Thomason.Subdivision.map_chainUnionMap line 188
  17. lemma OAI.Thomason.Subdivision.faceVertices_of_lt line 202
  18. lemma OAI.Thomason.Subdivision.initialFlag_map_faceVertices line 208
  19. lemma OAI.Thomason.Subdivision.extraVertexFace_highFace line 227
  20. lemma OAI.Thomason.Subdivision.extraVertex_highFace line 263
  21. lemma OAI.Thomason.Subdivision.chainLast_map line 290
  22. lemma OAI.Thomason.Subdivision.faceVertices_of_le line 294
  23. lemma OAI.Thomason.Subdivision.collapseVertices_succ_of_le line 299
  24. lemma OAI.Thomason.Subdivision.extraVertex_lowFace_saturated line 304
  25. lemma OAI.Thomason.Subdivision.extraVertex_lowFace_partialLastVertex line 321
  26. lemma OAI.Thomason.Subdivision.extraVertexMap_lowFace_partialLastMap line 338
  27. lemma OAI.Thomason.Subdivision.exPairSimplex_lowFace_level line 354
  28. lemma OAI.Thomason.Subdivision.partialLastVertex_map_absorb line 382
  29. lemma OAI.Thomason.Subdivision.partialLastMap_sd_absorb line 394
  30. lemma OAI.Thomason.Subdivision.exLevel_map_of line 408
  31. lemma OAI.Thomason.Subdivision.exLevel_highFace line 418
  32. lemma OAI.Thomason.Subdivision.exLevel_lowFace line 430
  33. lemma OAI.Thomason.Subdivision.extraVertexMap_highFace line 452
  34. lemma OAI.Thomason.Subdivision.exPairSimplex_highFace line 465
  35. lemma OAI.Thomason.Subdivision.chainUnionMap_comp line 474
  36. lemma OAI.Thomason.Subdivision.chainUnionMap_on_singleton line 484
  37. lemma OAI.Thomason.Subdivision.predAbove_castSucc_eq_succ line 496
  38. lemma OAI.Thomason.Subdivision.extraVertexFace_twice line 512
  39. lemma OAI.Thomason.Subdivision.extraVertex_twice line 538
  40. lemma OAI.Thomason.Subdivision.extraVertexMap_twice line 547
  41. lemma OAI.Thomason.Subdivision.exPairSimplex_twice line 559
  42. lemma OAI.Thomason.Subdivision.collapseVertices_face line 585
  43. lemma OAI.Thomason.Subdivision.initialFlag_map_collapseVertices line 589
  44. lemma OAI.Thomason.Subdivision.predAbove_eq_succ_low_iff line 603
  45. lemma OAI.Thomason.Subdivision.predAbove_eq_succ_high_iff line 626
  46. lemma OAI.Thomason.Subdivision.extraVertexFace_lowDegeneracy line 645
  47. lemma OAI.Thomason.Subdivision.extraVertexFace_highDegeneracy line 665
  48. lemma OAI.Thomason.Subdivision.extraVertex_lowDegeneracy line 688
  49. lemma OAI.Thomason.Subdivision.extraVertex_highDegeneracy line 698
  50. lemma OAI.Thomason.Subdivision.exLevel_exists_nat line 720
  51. def OAI.Thomason.Subdivision.exIndex line 724
  52. lemma OAI.Thomason.Subdivision.exIndex_level line 728
  53. lemma OAI.Thomason.Subdivision.exIndex_le_iff line 733
  54. lemma OAI.Thomason.Subdivision.exIndex_zero_iff line 742
  55. lemma OAI.Thomason.Subdivision.exIndex_pair line 747
  56. def OAI.Thomason.Subdivision.ExTypeI line 766
  57. def OAI.Thomason.Subdivision.ExTypeII line 771
  58. lemma OAI.Thomason.Subdivision.exPairSimplex_typeI line 774
  59. lemma OAI.Thomason.Subdivision.exTypeI_preimage_index line 778