OAI/CategoryTheory/Thomason/CoreCouniversality.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Core Couniversality.

  1. def OAI.Thomason.RelativePrismData.corePrismLeg line 20
  2. lemma OAI.Thomason.RelativePrismData.corePrismLeg_natural line 25
  3. lemma OAI.Thomason.RelativePrismData.corePrismLeg_endpoint_false line 43
  4. lemma OAI.Thomason.RelativePrismData.corePrismLeg_endpoint_true line 57
  5. lemma OAI.Thomason.RelativePrismData.corePrismLeg_stationary line 71
  6. def OAI.Thomason.RelativePrismData.corePrismCocone line 84
  7. def OAI.Thomason.RelativePrismData.corePrism line 92
  8. lemma OAI.Thomason.RelativePrismData.corePrism_leg line 97
  9. lemma OAI.Thomason.RelativePrismData.corePrism_endpoint_false line 104
  10. lemma OAI.Thomason.RelativePrismData.corePrism_endpoint_true line 121
  11. lemma OAI.Thomason.RelativePrismData.coreGrayPrism_stationary line 154
  12. lemma OAI.Thomason.RelativePrismData.coreGrayPrism_stationary_inclusion line 177
  13. def OAI.Thomason.RelativePrismData.coreFinitePrism line 200
  14. lemma OAI.Thomason.RelativePrismData.coreFinitePrism_unit line 208
  15. lemma OAI.Thomason.RelativePrismData.coreFinitePrism_endpoint_false line 215
  16. lemma OAI.Thomason.RelativePrismData.coreFinitePrism_endpoint_true line 230
  17. lemma OAI.Thomason.RelativePrismData.coreFinitePrism_stationary line 245
  18. def OAI.Thomason.RightIntervalCore.SimplexDescent line 283
  19. lemma OAI.Thomason.RightIntervalCore.intervalCore_simplexDescent_two line 287
  20. def OAI.Thomason.RightIntervalCore.simplexLift line 293
  21. lemma OAI.Thomason.RightIntervalCore.simplexLift_fac line 299
  22. lemma OAI.Thomason.RightIntervalCore.simplexLift_natural line 305
  23. lemma OAI.Thomason.RightIntervalCore.simplexLift_endpoint line 316
  24. def OAI.Thomason.RightIntervalCore.cutApply line 323
  25. lemma OAI.Thomason.RightIntervalCore.cutApply_natural line 327
  26. lemma OAI.Thomason.RightIntervalCore.cutApply_endpoint line 338
  27. def OAI.Thomason.RightIntervalCore.nerveCylinderSimplex line 346
  28. lemma OAI.Thomason.RightIntervalCore.nerveCylinderSimplex_natural line 352
  29. lemma OAI.Thomason.RightIntervalCore.nerveCylinderSimplex_endpoint line 368
  30. def OAI.Thomason.RightIntervalCore.nerveCylinder line 382
  31. lemma OAI.Thomason.RightIntervalCore.nerveCylinder_endpoint line 392
  32. def OAI.Thomason.RightIntervalCore.nerveHomotopy line 404
  33. lemma OAI.Thomason.RightIntervalCore.nerve_weak_iff line 418
  34. theorem OAI.Thomason.RightIntervalCore.finite_pushout_zigzag line 439
  35. theorem OAI.Thomason.GreatestNew.core_finite_pushout_deformation line 509
  36. theorem OAI.Thomason.GreatestNew.core_finite_pushout_nerve_weak line 544
  37. theorem OAI.Thomason.Couniversality.core_finite_poset_couniversal line 562
  38. theorem OAI.Thomason.Couniversality.core_poset_couniversal line 657
  39. lemma OAI.Thomason.AttachmentComparison.core_gray_piece_couniversal line 683
  40. lemma OAI.Thomason.AttachmentComparison.core_gray_comparison_local line 706