OAI/CategoryTheory/Thomason/GreatestAttachments.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Greatest Attachments.

  1. lemma OAI.Thomason.FiniteVertexChain.map_lift line 20
  2. def OAI.Thomason.RelativePrismData.prismLeg line 33
  3. lemma OAI.Thomason.RelativePrismData.prismLeg_natural line 38
  4. lemma OAI.Thomason.RelativePrismData.prismLeg_endpoint_false line 56
  5. lemma OAI.Thomason.RelativePrismData.prismLeg_endpoint_true line 70
  6. lemma OAI.Thomason.RelativePrismData.prismLeg_stationary line 84
  7. def OAI.Thomason.RelativePrismData.prismCocone line 97
  8. def OAI.Thomason.RelativePrismData.prism line 105
  9. lemma OAI.Thomason.RelativePrismData.prism_leg line 110
  10. lemma OAI.Thomason.RelativePrismData.prism_endpoint_false line 117
  11. lemma OAI.Thomason.RelativePrismData.prism_endpoint_true line 134
  12. def OAI.Thomason.SimplexIndex.postcompose line 163
  13. lemma OAI.Thomason.simplexVertexOrder_postcompose line 167
  14. lemma OAI.Thomason.RelativePrismData.grayPrism_stationary line 177
  15. lemma OAI.Thomason.RelativePrismData.grayPrism_stationary_inclusion line 200
  16. def OAI.Thomason.RelativePrismData.finitePrism line 223
  17. lemma OAI.Thomason.RelativePrismData.finitePrism_unit line 231
  18. lemma OAI.Thomason.RelativePrismData.finitePrism_endpoint_false line 238
  19. lemma OAI.Thomason.RelativePrismData.finitePrism_endpoint_true line 253
  20. lemma OAI.Thomason.RelativePrismData.finitePrism_stationary line 268
  21. def OAI.Thomason.GreatestNew.retract line 308
  22. def OAI.Thomason.GreatestNew.upper line 319
  23. lemma OAI.Thomason.GreatestNew.retract_old line 330
  24. lemma OAI.Thomason.GreatestNew.upper_old line 334
  25. lemma OAI.Thomason.GreatestNew.retract_comp_inc line 338
  26. lemma OAI.Thomason.GreatestNew.id_le_upper line 343
  27. lemma OAI.Thomason.GreatestNew.retract_le_upper line 349
  28. lemma OAI.Thomason.GreatestNew.upper_constant line 357
  29. def OAI.Thomason.GreatestNew.idPrismData line 362
  30. def OAI.Thomason.GreatestNew.retractPrismData line 370
  31. theorem OAI.Thomason.RightIntervalExtension.finite_pushout_zigzag line 396
  32. lemma OAI.Thomason.RightIntervalExtension.finite_nerve_weak_of_zigzag line 447
  33. lemma OAI.Thomason.GreatestNew.finitePosetMap_id line 473
  34. lemma OAI.Thomason.GreatestNew.finitePosetMap_comp line 477
  35. theorem OAI.Thomason.GreatestNew.finite_pushout_deformation line 490
  36. theorem OAI.Thomason.GreatestNew.finite_pushout_nerve_weak line 525
  37. lemma OAI.Thomason.RightIntervalExtension.omegaCylinder_pushout line 550
  38. def OAI.Thomason.RightIntervalExtension.omegaGlue line 555
  39. lemma OAI.Thomason.RightIntervalExtension.omegaGlue_left line 559
  40. lemma OAI.Thomason.RightIntervalExtension.omegaGlue_right line 564
  41. lemma OAI.Thomason.RightIntervalExtension.omegaCylinder_hom_ext line 570
  42. lemma OAI.Thomason.RightIntervalExtension.omegaGlue_endpoint_left line 575
  43. lemma OAI.Thomason.RightIntervalExtension.omegaGlue_endpoint_right line 584
  44. theorem OAI.Thomason.RightIntervalExtension.omega_stationary_gluing line 595
  45. lemma OAI.Thomason.RightIntervalExtension.omega_stationary_gluing_natural line 630
  46. theorem OAI.Thomason.RightIntervalExtension.omega_pushout_zigzag line 669
  47. lemma OAI.Thomason.RightIntervalExtension.omega_nerve_weak_of_zigzag line 720
  48. abbrev OAI.Thomason.GreatestNew.omegaPosetObj line 746
  49. abbrev OAI.Thomason.GreatestNew.omegaPosetMap line 749
  50. abbrev OAI.Thomason.GreatestNew.omegaInc line 753
  51. lemma OAI.Thomason.GreatestNew.omegaPosetMap_id line 756
  52. lemma OAI.Thomason.GreatestNew.omegaPosetMap_comp line 760
  53. theorem OAI.Thomason.GreatestNew.omega_pushout_deformation line 772
  54. theorem OAI.Thomason.GreatestNew.omega_pushout_nerve_weak line 807