OAI/CategoryTheory/Thomason/Couniversality.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Couniversality.

  1. lemma OAI.Thomason.Couniversality.greatest_or_two_maximal line 15
  2. lemma OAI.Thomason.Couniversality.maximal_new_isMax line 30
  3. lemma OAI.Thomason.Couniversality.delete_max_lower line 35
  4. def OAI.Thomason.Couniversality.nestedOldIso line 43
  5. lemma OAI.Thomason.Couniversality.nestedOldIso_inc line 57
  6. lemma OAI.Thomason.Couniversality.restricted_lower line 65
  7. def OAI.Thomason.Couniversality.restrictedRetract line 69
  8. lemma OAI.Thomason.Couniversality.restricted_adjoint line 74
  9. lemma OAI.Thomason.Couniversality.weak_of_full_sieve_cover line 82
  10. lemma OAI.Thomason.Couniversality.isIso_subtype_all line 121
  11. theorem OAI.Thomason.Couniversality.finite_poset_couniversal line 128
  12. theorem OAI.Thomason.Couniversality.omega_finite_poset_couniversal line 223
  13. lemma OAI.Thomason.AttachmentComparison.finite_nerve_attachment_mono line 317
  14. lemma OAI.Thomason.AttachmentComparison.finite_nerve_upper_mono line 333
  15. lemma OAI.Thomason.AttachmentComparison.finite_nerve_inter_upper_mono line 353
  16. lemma OAI.Thomason.AttachmentComparison.finite_piece_couniversal line 370
  17. lemma OAI.Thomason.AttachmentComparison.comparison_local_finite_poset line 393
  18. lemma OAI.Thomason.FilteredWeak.colimit_lifting line 498
  19. lemma OAI.Thomason.FilteredWeak.boundary_rlp_colimit line 522
  20. lemma OAI.Thomason.FilteredWeak.eval₀_rlp line 528
  21. lemma OAI.Thomason.FilteredWeak.path_projection_rlp line 548
  22. lemma OAI.Thomason.FilteredWeak.path_map_id line 553
  23. lemma OAI.Thomason.FilteredWeak.const_natural line 558
  24. lemma OAI.Thomason.FilteredWeak.path_map_left line 564
  25. def OAI.Thomason.FilteredWeak.pathDiagram line 574
  26. def OAI.Thomason.FilteredWeak.pathProjection line 585
  27. def OAI.Thomason.FilteredWeak.pathLeft line 590
  28. def OAI.Thomason.FilteredWeak.pathRight line 595
  29. lemma OAI.Thomason.FilteredWeak.path_left_projection line 600
  30. lemma OAI.Thomason.FilteredWeak.path_fac line 607
  31. theorem OAI.Thomason.FilteredWeak.kan_colimit_weak line 613
  32. theorem OAI.Thomason.FilteredWeak.colimit_weak line 638
  33. lemma OAI.Thomason.FilteredWeak.weak_of_colimit line 657