OAI/CategoryTheory/Thomason/PosetalReduction.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Posetal Reduction.

  1. inductive OAI.Thomason.GeometricRecognition.PosetAttachment.Obj line 17
  2. def OAI.Thomason.GeometricRecognition.PosetAttachment.Rel line 21
  3. instance OAI.Thomason.GeometricRecognition.PosetAttachment.partialOrder line 27
  4. def OAI.Thomason.GeometricRecognition.PosetAttachment.left line 60
  5. def OAI.Thomason.GeometricRecognition.PosetAttachment.right line 64
  6. theorem OAI.Thomason.GeometricRecognition.PosetAttachment.agree line 84
  7. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.agree_natural line 86
  8. def OAI.Thomason.GeometricRecognition.PosetAttachment.obj line 93
  9. def OAI.Thomason.GeometricRecognition.PosetAttachment.bridge line 97
  10. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.bridge_eq line 108
  11. def OAI.Thomason.GeometricRecognition.PosetAttachment.arrow line 125
  12. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.arrow_trans line 131
  13. def OAI.Thomason.GeometricRecognition.PosetAttachment.desc line 166
  14. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.left_desc line 172
  15. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.right_obj_desc line 177
  16. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.right_mem line 184
  17. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.right_not_mem line 187
  18. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.arrow_heq line 190
  19. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.right_desc line 195
  20. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.square line 223
  21. lemma OAI.Thomason.GeometricRecognition.PosetAttachment.joint_ext line 229
  22. theorem OAI.Thomason.GeometricRecognition.PosetAttachment.isPushout line 284
  23. lemma OAI.Thomason.GeometricRecognition.Posetal.pushout_posetal line 318
  24. abbrev OAI.Thomason.GeometricRecognition.Posetal.CC line 342
  25. lemma OAI.Thomason.GeometricRecognition.Posetal.initial_posetal line 344
  26. lemma OAI.Thomason.GeometricRecognition.Posetal.boundary_posetal_successor line 353
  27. lemma OAI.Thomason.GeometricRecognition.Posetal.skeleton_posetal line 395
  28. theorem OAI.Thomason.GeometricRecognition.Posetal.categorification_sdTwice_posetal line 410
  29. def OAI.Thomason.KanLocal.transpose line 444
  30. lemma OAI.Thomason.KanLocal.transpose_transpose line 447
  31. lemma OAI.Thomason.KanLocal.transpose_homotopic line 454
  32. lemma OAI.Thomason.KanLocal.transpose_pre line 458
  33. lemma OAI.Thomason.KanLocal.transpose_post line 465
  34. lemma OAI.Thomason.KanLocal.local_of_homotopy_classes line 471
  35. lemma OAI.Thomason.KanLocal.lastVertex_local line 492
  36. lemma OAI.Thomason.KanLocal.local_of_precomp line 496
  37. lemma OAI.Thomason.KanLocal.local_of_postcomp line 503
  38. theorem OAI.Thomason.GeometricRecognition.Posetal.kan_poset_replacement line 521
  39. lemma OAI.Thomason.GeometricRecognition.kan_local_heq line 545
  40. lemma OAI.Thomason.GeometricRecognition.kan_ex_poset_replacement line 551
  41. lemma OAI.Thomason.GeometricRecognition.relative_representative line 562
  42. lemma OAI.Thomason.GeometricRecognition.finite_relative_stage line 590