OAI/CategoryTheory/Thomason/ExtensionAnodyne.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Extension Anodyne.

  1. lemma OAI.Thomason.Subdivision.nonDegenerate_of_unique_face line 16
  2. lemma OAI.Thomason.Subdivision.exPairSimplex_face_unique line 43
  3. lemma OAI.Thomason.Subdivision.exPairSimplex_nonDegenerate line 80
  4. lemma OAI.Thomason.Subdivision.extraVertexMap_lowDegeneracy line 98
  5. lemma OAI.Thomason.Subdivision.extraVertexMap_highDegeneracy line 110
  6. lemma OAI.Thomason.Subdivision.exPairSimplex_lowDegeneracy line 122
  7. lemma OAI.Thomason.Subdivision.exPairSimplex_highDegeneracy line 131
  8. lemma OAI.Thomason.Subdivision.exLevel_highDegeneracy line 140
  9. lemma OAI.Thomason.Subdivision.exIndex_degeneracy_ne_self line 154
  10. lemma OAI.Thomason.Subdivision.exPairSimplex_reflects_nonDegenerate line 175
  11. lemma OAI.Thomason.Subdivision.exPairSimplex_input_not_typeI line 214
  12. lemma OAI.Thomason.Subdivision.exTypeI_preimage_typeII line 225
  13. lemma OAI.Thomason.Subdivision.exPairSimplex_injective line 240
  14. abbrev OAI.Thomason.Subdivision.ExPairIndices line 265
  15. lemma OAI.Thomason.Subdivision.exIndex_pos_of_notMem line 267
  16. lemma OAI.Thomason.Subdivision.exIndex_notMem_of_pos line 276
  17. def OAI.Thomason.Subdivision.exPairingCore line 283
  18. instance OAI.Thomason.Subdivision.exPairingCore_isProper line 337
  19. lemma OAI.Thomason.Subdivision.exPairSimplex_other_face_index_lt line 359
  20. def OAI.Thomason.Subdivision.exPairRank line 415
  21. lemma OAI.Thomason.Subdivision.exPairRank_decreases line 418
  22. instance OAI.Thomason.Subdivision.exPairingCore_isRegular line 445
  23. theorem OAI.Thomason.Subdivision.exComparison_strongAnodyne line 448
  24. lemma OAI.Thomason.Subdivision.exComparison_anodyne line 464
  25. theorem OAI.Thomason.Subdivision.exComparison_weak line 467
  26. theorem OAI.Thomason.Subdivision.ex_map_weak_iff line 482
  27. lemma OAI.Thomason.Subdivision.exSquared_map_weak_iff line 493
  28. lemma OAI.Thomason.Subdivision.thomasonWeak_iff_nerve line 498
  29. lemma OAI.Thomason.Subdivision.thomasonWeakFinite_iff_nerve line 503
  30. def OAI.Thomason.Subdivision.flagOldLast line 522
  31. lemma OAI.Thomason.Subdivision.flagOldLast_mono line 526
  32. lemma OAI.Thomason.Subdivision.le_flagOldLast line 530
  33. lemma OAI.Thomason.Subdivision.flagOldLast_of_old line 536
  34. def OAI.Thomason.Subdivision.conicalFlagRetraction line 545
  35. lemma OAI.Thomason.Subdivision.conicalFlagRetraction_old line 582
  36. lemma OAI.Thomason.Subdivision.conicalFlagRetraction_map_old line 589
  37. def OAI.Thomason.Subdivision.HornFaces line 612
  38. def OAI.Thomason.Subdivision.hornFacePoint line 615
  39. def OAI.Thomason.Subdivision.hornFaceCone line 625
  40. lemma OAI.Thomason.Subdivision.le_hornFaceCone line 637
  41. lemma OAI.Thomason.Subdivision.hornFacePoint_le_cone line 642
  42. def OAI.Thomason.Subdivision.hornFlagRetraction line 652
  43. lemma OAI.Thomason.Subdivision.hornFlagRetraction_old line 657
  44. lemma OAI.Thomason.Subdivision.allowedChains_iff line 662
  45. lemma OAI.Thomason.Subdivision.orderedSimplexSubcomplex_mem_iff line 679
  46. lemma OAI.Thomason.Subdivision.hornFaces_allowed_iff line 697
  47. def OAI.Thomason.Subdivision.hornFacesIso line 715
  48. lemma OAI.Thomason.Subdivision.simplexVertices_yoneda line 737
  49. lemma OAI.Thomason.Subdivision.lastVertex_nerve line 747
  50. lemma OAI.Thomason.Subdivision.sdSubcomplex_lastVertex line 765
  51. lemma OAI.Thomason.Subdivision.sdTwiceSubcomplex_lastVertex line 771