OAI/CategoryTheory/Thomason/AttachmentComparison.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Attachment Comparison.

  1. def OAI.Thomason.FilteredPosets.nerveIsColimit line 15
  2. def OAI.Thomason.FilteredPosets.diagram line 50
  3. def OAI.Thomason.FilteredPosets.cocone line 58
  4. def OAI.Thomason.FilteredPosets.unionIsColimit line 65
  5. def OAI.Thomason.FilteredPosets.oldDiagram line 75
  6. def OAI.Thomason.FilteredPosets.oldCocone line 84
  7. def OAI.Thomason.FilteredPosets.inclusion line 91
  8. def OAI.Thomason.FilteredPosets.oldUnionIsColimit line 96
  9. def OAI.Thomason.FilteredPosets.close line 108
  10. lemma OAI.Thomason.FilteredPosets.mem_close line 112
  11. lemma OAI.Thomason.FilteredPosets.close_contains line 117
  12. lemma OAI.Thomason.FilteredPosets.close_stable line 121
  13. def OAI.Thomason.FilteredPosets.closedFamily line 129
  14. instance OAI.Thomason.FilteredPosets.closedFamily_finite line 138
  15. lemma OAI.Thomason.FilteredPosets.closedFamily_cover line 141
  16. def OAI.Thomason.FilteredPushouts.isColimitOfPushout line 156
  17. abbrev OAI.Thomason.FilteredPushouts.attachingMap line 211
  18. abbrev OAI.Thomason.FilteredPushouts.attachmentDiagram line 214
  19. def OAI.Thomason.FilteredPushouts.attachmentCocone line 216
  20. lemma OAI.Thomason.FilteredPushouts.attachmentCocone_inl line 226
  21. lemma OAI.Thomason.FilteredPushouts.attachmentCocone_inr line 235
  22. def OAI.Thomason.FilteredPushouts.attachmentIsColimit line 243
  23. theorem OAI.Thomason.Couniversality.couniversal_of_finite line 272
  24. theorem OAI.Thomason.Couniversality.poset_couniversal line 329
  25. theorem OAI.Thomason.Couniversality.omega_poset_couniversal line 344
  26. lemma OAI.Thomason.AttachmentComparison.gray_piece_couniversal line 369
  27. lemma OAI.Thomason.AttachmentComparison.gray_comparison_local line 392
  28. abbrev OAI.Thomason.OmegaAttachmentComparison.posetObj line 497
  29. abbrev OAI.Thomason.OmegaAttachmentComparison.sb line 498
  30. abbrev OAI.Thomason.OmegaAttachmentComparison.inc line 500
  31. lemma OAI.Thomason.OmegaAttachmentComparison.sb_inc line 503
  32. lemma OAI.Thomason.OmegaAttachmentComparison.attachment_nerve_cover line 508
  33. lemma OAI.Thomason.OmegaAttachmentComparison.poset_nerve_cover line 556
  34. lemma OAI.Thomason.OmegaAttachmentComparison.nerve_attachment_mono line 576
  35. lemma OAI.Thomason.OmegaAttachmentComparison.nerve_upper_mono line 589
  36. lemma OAI.Thomason.OmegaAttachmentComparison.nerve_inter_upper_mono line 608
  37. lemma OAI.Thomason.OmegaAttachmentComparison.gray_piece_couniversal line 624
  38. lemma OAI.Thomason.OmegaAttachmentComparison.gray_comparison_local line 646