OAI/CategoryTheory/Thomason/ProperTransfer.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Proper Transfer.

  1. abbrev OAI.Thomason.AbstractTransfer.Boundaries.arrow line 26
  2. def OAI.Thomason.AbstractTransfer.Boundaries.Admissible line 28
  3. instance OAI.Thomason.AbstractTransfer.Boundaries.(instance at line 31) line 31
  4. lemma OAI.Thomason.AbstractTransfer.Boundaries.boundary_admissible line 37
  5. def OAI.Thomason.AbstractTransfer.Boundaries.posetCoprodIso line 57
  6. def OAI.Thomason.AbstractTransfer.Boundaries.oldCoprodIso line 62
  7. lemma OAI.Thomason.AbstractTransfer.Boundaries.posetCoprodIso_ι line 66
  8. lemma OAI.Thomason.AbstractTransfer.Boundaries.oldCoprodIso_ι line 73
  9. lemma OAI.Thomason.AbstractTransfer.Boundaries.coprod_inc line 84
  10. instance OAI.Thomason.AbstractTransfer.Boundaries.admissible_coproducts line 99
  11. instance OAI.Thomason.AbstractTransfer.Boundaries.(instance at line 122) line 122
  12. lemma OAI.Thomason.AbstractTransfer.Boundaries.poset_attachment_invariance line 128
  13. lemma OAI.Thomason.AbstractTransfer.Boundaries.admissible_pushout_mono line 171
  14. lemma OAI.Thomason.AbstractTransfer.Boundaries.admissible_pushout_weak line 189
  15. lemma OAI.Thomason.AbstractTransfer.Boundaries.coproduct_boundary_pushout_mono line 209
  16. lemma OAI.Thomason.AbstractTransfer.Boundaries.coproduct_boundary_pushout_weak line 217
  17. abbrev OAI.Thomason.AbstractTransfer.Boundaries.Cells line 246
  18. lemma OAI.Thomason.AbstractTransfer.Boundaries.weak_iso line 250
  19. lemma OAI.Thomason.AbstractTransfer.Boundaries.sequential_pushout_weak line 255
  20. lemma OAI.Thomason.AbstractTransfer.Boundaries.cofibration_pushout_weak line 353
  21. theorem OAI.Thomason.AbstractTransfer.Boundaries.left_proper line 402
  22. lemma OAI.Thomason.AbstractTransfer.unit_weak line 428
  23. theorem OAI.Thomason.AbstractTransfer.adjoint_weak_iff line 437
  24. lemma OAI.Thomason.AbstractTransfer.left_preserves_weak line 445
  25. def OAI.Thomason.AbstractTransfer.exactEndpoint line 459
  26. theorem OAI.Thomason.omegaPosetComparison line 491
  27. theorem OAI.Thomason.finitePosetComparison line 498
  28. def OAI.Thomason.omegaEndpointOfGray line 508
  29. def OAI.Thomason.finiteEndpointOfGray line 516
  30. theorem OAI.Thomason.fullMain_of_rightIntervalExtension line 525
  31. inductive OAI.Thomason.GrayRecursive.RectangleCell line 540
  32. def OAI.Thomason.GrayRecursive.RectangleCell.eval line 545
  33. def OAI.Thomason.GrayRecursive.intervalLabel line 550
  34. lemma OAI.Thomason.GrayRecursive.intervalLabel_end line 553
  35. lemma OAI.Thomason.GrayRecursive.intervalLabel_vertical line 559
  36. lemma OAI.Thomason.GrayRecursive.intervalLabel_up line 564
  37. lemma OAI.Thomason.GrayRecursive.project_end line 569
  38. lemma OAI.Thomason.GrayRecursive.project_vertical_vertex line 576
  39. lemma OAI.Thomason.GrayRecursive.vertex_label line 587
  40. lemma OAI.Thomason.GrayRecursive.project_up_label line 591
  41. lemma OAI.Thomason.GrayRecursive.vertex_injective line 596
  42. lemma OAI.Thomason.GrayRecursive.RectangleCell.eval_injective line 602
  43. lemma OAI.Thomason.GrayRecursive.RectangleCell.eval_surjective line 642
  44. def OAI.Thomason.GrayRecursive.rectangleEquiv line 649
  45. lemma OAI.Thomason.GrayRecursive.rectangleEquiv_apply line 652
  46. lemma OAI.Thomason.GrayRecursive.globe_succ_cases line 666
  47. lemma OAI.Thomason.GrayRecursive.atEnd_truncate line 673
  48. lemma OAI.Thomason.GrayRecursive.vertex_truncate line 677
  49. lemma OAI.Thomason.GrayRecursive.edge_truncate_zero line 681
  50. lemma OAI.Thomason.GrayRecursive.edge_truncate_succ line 689
  51. lemma OAI.Thomason.GrayRecursive.up_truncate_zero line 696
  52. lemma OAI.Thomason.GrayRecursive.up_truncate_succ line 704
  53. lemma OAI.Thomason.GrayRecursive.suspend_truncate_zero line 707
  54. lemma OAI.Thomason.GrayRecursive.atEnd_vertex_eq line 712
  55. lemma OAI.Thomason.GrayRecursive.nonobject_cases line 723
  56. def OAI.Thomason.GrayRecursive.RectangleCell.truncate line 736
  57. lemma OAI.Thomason.GrayRecursive.RectangleCell.eval_truncate line 741
  58. lemma OAI.Thomason.GrayRecursive.positive_matching_iff line 745