OAI/CategoryTheory/Thomason/FiniteAttachments.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Finite Attachments.

  1. theorem OAI.Thomason.Attachments.cosieve_attachment_covers line 15
  2. def OAI.Thomason.Attachments.fullFinite line 87
  3. def OAI.Thomason.Attachments.fullFiniteInclusion line 90
  4. def OAI.Thomason.Attachments.IsPosetFiniteAttachmentPiece line 93
  5. def OAI.Thomason.Attachments.IsPosetFiniteNewPiece line 104
  6. lemma OAI.Thomason.Attachments.posetFiniteLabel_constant line 122
  7. lemma OAI.Thomason.Attachments.posetFiniteLabel_natural line 130
  8. lemma OAI.Thomason.Attachments.posetFiniteLabel_max line 137
  9. lemma OAI.Thomason.Attachments.posetFiniteLabel_min line 145
  10. def OAI.Thomason.Attachments.constantFiniteLabel line 153
  11. lemma OAI.Thomason.Attachments.comp_constantFiniteLabel line 156
  12. def OAI.Thomason.Attachments.constantFiniteAttachmentLabel line 168
  13. lemma OAI.Thomason.Attachments.constantFiniteAttachmentLabel_old line 173
  14. lemma OAI.Thomason.Attachments.constantFiniteAttachmentLabel_new line 175
  15. lemma OAI.Thomason.Attachments.subposetFiniteMap_comp line 178
  16. lemma OAI.Thomason.Attachments.fiberFiniteInclusion_mono line 185
  17. def OAI.Thomason.Attachments.intervalFiberFullFiniteIso line 194
  18. lemma OAI.Thomason.Attachments.constant_finite_attachment_old_piece line 201
  19. lemma OAI.Thomason.Attachments.constant_finite_attachment_new_piece line 245
  20. def OAI.Thomason.Attachments.finitePosetObject line 292
  21. lemma OAI.Thomason.Attachments.posetFiniteLabel_objects line 297
  22. lemma OAI.Thomason.Attachments.labelled_finite_objects_cover line 304
  23. def OAI.Thomason.Attachments.maxFiniteLabel line 342
  24. def OAI.Thomason.Attachments.minFiniteLabel line 345
  25. lemma OAI.Thomason.Attachments.comp_maxFiniteLabel line 348
  26. lemma OAI.Thomason.Attachments.comp_minFiniteLabel line 352
  27. lemma OAI.Thomason.Attachments.maxFiniteLabel_objects_fiber line 356
  28. lemma OAI.Thomason.Attachments.minFiniteLabel_objects_fiber line 361
  29. theorem OAI.Thomason.Attachments.sieve_finite_attachment_covers line 366
  30. theorem OAI.Thomason.Attachments.cosieve_finite_attachment_covers line 436