OAI/CategoryTheory/Thomason/ModelClasses.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Model Classes.

  1. structure OAI.Thomason.OmegaCategory.LimitCell line 32
  2. def OAI.Thomason.OmegaCategory.LimitCell.source line 41
  3. def OAI.Thomason.OmegaCategory.LimitCell.target line 46
  4. lemma OAI.Thomason.OmegaCategory.LimitCell.composable line 51
  5. def OAI.Thomason.OmegaCategory.LimitCell.comp line 55
  6. def OAI.Thomason.OmegaCategory.limitCategory line 76
  7. def OAI.Thomason.OmegaCategory.limitProjection line 124
  8. def OAI.Thomason.OmegaCategory.limitLift line 130
  9. def OAI.Thomason.OmegaCategory.boundedLimitCone line 148
  10. def OAI.Thomason.OmegaCategory.boundedLimitConeIsLimit line 157
  11. instance OAI.Thomason.OmegaCategory.hasLimits line 169
  12. instance OAI.Thomason.OmegaCategory.nCategory_hasLimits line 185
  13. instance OAI.Thomason.OmegaCategory.nCategoryInclusion_preservesLimits line 188
  14. lemma OAI.Thomason.NormalizedChains.faces_zero line 204
  15. def OAI.Thomason.NormalizedChains.awZeroWord line 210
  16. def OAI.Thomason.NormalizedChains.awEdgeWord line 213
  17. lemma OAI.Thomason.NormalizedChains.awEdgeWord_nil line 218
  18. lemma OAI.Thomason.NormalizedChains.awEdgeWord_append line 220
  19. lemma OAI.Thomason.NormalizedChains.awZeroWord_of_all line 224
  20. lemma OAI.Thomason.NormalizedChains.awZeroWord_of_not_all line 227
  21. lemma OAI.Thomason.NormalizedChains.awZeroWord_append_of_ne line 230
  22. lemma OAI.Thomason.NormalizedChains.all_zero_of_last_zero line 236
  23. lemma OAI.Thomason.NormalizedChains.awEdgeWord_of_all line 243
  24. lemma OAI.Thomason.NormalizedChains.boundary_awZeroWord line 249
  25. lemma OAI.Thomason.NormalizedChains.boundary_awEdgeWord line 270
  26. def OAI.Thomason.NormalizedChains.awZero line 312
  27. def OAI.Thomason.NormalizedChains.awEdge line 315
  28. lemma OAI.Thomason.NormalizedChains.awZeroWord_eq_zero_of_not_pairwise line 318
  29. lemma OAI.Thomason.NormalizedChains.awEdgeWord_eq_zero_of_not_pairwise line 323
  30. lemma OAI.Thomason.NormalizedChains.awZero_bracket line 347
  31. lemma OAI.Thomason.NormalizedChains.awEdge_bracket line 357
  32. lemma OAI.Thomason.NormalizedChains.awZero_wordBoundary line 368
  33. lemma OAI.Thomason.NormalizedChains.awEdge_wordBoundary line 377
  34. lemma OAI.Thomason.NormalizedChains.awEdge_boundary line 386
  35. lemma OAI.Thomason.NormalizedChains.awZeroWord_positive line 404
  36. lemma OAI.Thomason.NormalizedChains.awEdgeWord_positive line 410
  37. lemma OAI.Thomason.NormalizedChains.awZero_positive line 419
  38. lemma OAI.Thomason.NormalizedChains.awEdge_positive line 422
  39. lemma OAI.Thomason.NormalizedChains.awOne_positive line 425
  40. lemma OAI.Thomason.NormalizedChains.awZeroWord_mem_grade line 448
  41. lemma OAI.Thomason.NormalizedChains.awEdgeWord_mem_grade line 454
  42. lemma OAI.Thomason.NormalizedChains.awZero_mem_grade line 463
  43. lemma OAI.Thomason.NormalizedChains.awEdge_mem_grade line 469
  44. lemma OAI.Thomason.NormalizedChains.boundary_awZero line 487
  45. lemma OAI.Thomason.NormalizedChains.boundary_awZero_of_grade line 515
  46. def OAI.Thomason.NormalizedChains.awMap line 519
  47. def OAI.Thomason.NormalizedChains.awHom line 561