OAI/CategoryTheory/Thomason/PartialTables.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Partial Tables.

  1. def OAI.Thomason.DirectedComplex.PartialHom.image line 17
  2. lemma OAI.Thomason.DirectedComplex.PartialHom.image_source line 20
  3. lemma OAI.Thomason.DirectedComplex.PartialHom.image_source_n line 26
  4. lemma OAI.Thomason.DirectedComplex.PartialHom.image_target_lt line 30
  5. lemma OAI.Thomason.DirectedComplex.PartialHom.image_composable line 36
  6. lemma OAI.Thomason.DirectedComplex.PartialHom.image_comp_lt line 41
  7. lemma OAI.Thomason.DirectedComplex.PartialHom.image_boundary_of_bounded line 49
  8. lemma OAI.Thomason.DirectedComplex.PartialHom.image_boundary_comp line 53
  9. lemma OAI.Thomason.DirectedComplex.PartialHom.image_boundary_of_atoms line 76
  10. def OAI.Thomason.DirectedComplex.PartialHom.extendOriental line 103
  11. def OAI.Thomason.PartialNormalized.homWord line 156
  12. def OAI.Thomason.PartialNormalized.homTotal line 160
  13. lemma OAI.Thomason.PartialNormalized.homTotal_bracket line 163
  14. lemma OAI.Thomason.PartialNormalized.homTotal_grade line 179
  15. lemma OAI.Thomason.PartialNormalized.homTotal_map line 188
  16. lemma OAI.Thomason.PartialNormalized.homTotal_positive line 209
  17. lemma OAI.Thomason.PartialNormalized.homTotal_boundary line 217
  18. lemma OAI.Thomason.PartialNormalized.homTotal_vertex_exists line 252
  19. def OAI.Thomason.PartialNormalized.homVertex line 262
  20. lemma OAI.Thomason.PartialNormalized.homTotal_vertex line 265
  21. lemma OAI.Thomason.PartialNormalized.homVertex_monotone line 269
  22. def OAI.Thomason.PartialNormalized.homVertexOrderHom line 279
  23. lemma OAI.Thomason.PartialNormalized.homTotal_bracket_supportedOn_lower line 282
  24. def OAI.Thomason.PartialNormalized.cutWord line 308
  25. lemma OAI.Thomason.PartialNormalized.cutWord_nil line 312
  26. lemma OAI.Thomason.PartialNormalized.cutWord_append line 317
  27. lemma OAI.Thomason.PartialNormalized.cutWord_of_all_zero line 322
  28. lemma OAI.Thomason.PartialNormalized.cutWord_positive line 328
  29. lemma OAI.Thomason.PartialNormalized.cutWord_grade line 338
  30. lemma OAI.Thomason.PartialNormalized.cutWord_supportedOn_lower line 348
  31. lemma OAI.Thomason.PartialNormalized.cutWord_boundary line 361
  32. lemma OAI.Thomason.PartialNormalized.cutWord_eq_zero_of_not_pairwise line 398
  33. def OAI.Thomason.PartialNormalized.cutTotal line 430
  34. lemma OAI.Thomason.PartialNormalized.cutTotal_bracket line 433
  35. lemma OAI.Thomason.PartialNormalized.cutTotal_grade line 442
  36. lemma OAI.Thomason.PartialNormalized.cutTotal_positive line 448
  37. lemma OAI.Thomason.PartialNormalized.cutTotal_wordBoundary line 452
  38. lemma OAI.Thomason.PartialNormalized.cutTotal_boundary line 462
  39. lemma OAI.Thomason.PartialNormalized.cutTotal_empty line 476
  40. lemma OAI.Thomason.PartialNormalized.cutTotal_augmentation line 480
  41. def OAI.Thomason.PartialNormalized.cutHom line 487
  42. def OAI.Thomason.DirectedComplex.PartialHom.oneStep line 509
  43. lemma OAI.Thomason.DirectedComplex.PartialHom.table_eq_oneStep_source line 531
  44. lemma OAI.Thomason.DirectedComplex.PartialHom.table_target_eq_oneStep_target line 538
  45. lemma OAI.Thomason.DirectedComplex.PartialHom.image_boundary_of_oneStep line 546
  46. lemma OAI.Thomason.liftedChainMap_d_below line 571
  47. def OAI.Thomason.liftedPartial line 587
  48. lemma OAI.Thomason.liftedMap_atom_row line 597
  49. lemma OAI.Thomason.liftedPartial_table_atom line 660
  50. lemma OAI.Thomason.liftedPartial_image line 683
  51. lemma OAI.Thomason.oriental_functor_ext_truncated line 707
  52. lemma OAI.Thomason.PartialNormalized.cutWord_boundary_append_one line 739
  53. lemma OAI.Thomason.PartialNormalized.cutTotal_eq_homTotal_of_supported line 756
  54. lemma OAI.Thomason.PartialNormalized.cutHom_table_of_supported line 770
  55. lemma OAI.Thomason.PartialNormalized.cutHom_image_of_supported line 783
  56. lemma OAI.Thomason.PartialNormalized.truncate_supported line 790