OAI/CategoryTheory/Thomason/SimplexRanks.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Simplex Ranks.

  1. def OAI.Thomason.NormalizedChains.simplexRank line 14
  2. lemma OAI.Thomason.NormalizedChains.simplexWeight_lt line 18
  3. lemma OAI.Thomason.NormalizedChains.simplexRank_bounds line 24
  4. lemma OAI.Thomason.NormalizedChains.simplexRank_tail_lt line 36
  5. lemma OAI.Thomason.NormalizedChains.prepend_apply_cons line 48
  6. lemma OAI.Thomason.NormalizedChains.wordBoundary_rank line 62
  7. lemma OAI.Thomason.NormalizedChains.boundary_apply line 114
  8. lemma OAI.Thomason.NormalizedChains.simplex_peel_positive line 121
  9. lemma OAI.Thomason.NormalizedChains.simplex_peel_remainder line 154
  10. def OAI.Thomason.DirectedComplex.Table.extensionRow line 177
  11. lemma OAI.Thomason.DirectedComplex.Table.extensionRow_top line 181
  12. lemma OAI.Thomason.DirectedComplex.Table.extensionRow_middle line 184
  13. lemma OAI.Thomason.DirectedComplex.Table.extensionRow_other line 188
  14. def OAI.Thomason.DirectedComplex.Table.extendTop line 192
  15. lemma OAI.Thomason.DirectedComplex.Table.extendTop_row line 241
  16. lemma OAI.Thomason.DirectedComplex.Table.extendTop_source line 246
  17. lemma OAI.Thomason.DirectedComplex.Table.extendTop_dimension line 263
  18. lemma OAI.Thomason.DirectedComplex.Table.eq_extendTop line 277
  19. def OAI.Thomason.NormalizedChains.chainMass line 314
  20. lemma OAI.Thomason.NormalizedChains.chainMass_eq_sum line 316
  21. lemma OAI.Thomason.NormalizedChains.chainMass_bracket line 322
  22. lemma OAI.Thomason.NormalizedChains.chainMass_nonneg line 326
  23. lemma OAI.Thomason.NormalizedChains.chainMass_pos line 331
  24. def OAI.Thomason.NormalizedChains.Executable line 337
  25. lemma OAI.Thomason.NormalizedChains.positive_chain_execution line 341
  26. lemma OAI.Thomason.DirectedComplex.Table.ext_source_top line 385
  27. lemma OAI.Thomason.DirectedComplex.Table.fixed_of_top_zero line 394
  28. lemma OAI.Thomason.DirectedComplex.Table.comp_dimension line 416
  29. lemma OAI.Thomason.DirectedComplex.Table.split_top line 425
  30. inductive OAI.Thomason.NormalizedChains.TopPasting line 464
  31. lemma OAI.Thomason.NormalizedChains.oriental_top_pasting line 471
  32. def OAI.Thomason.WeakHomotopy.basedLoopMap line 532
  33. def OAI.Thomason.WeakHomotopy.basedGroupMap line 536
  34. lemma OAI.Thomason.WeakHomotopy.basedGroupMap_comp line 540
  35. lemma OAI.Thomason.WeakHomotopy.basedGroupMap_id line 548
  36. lemma OAI.Thomason.WeakHomotopy.basedGroupMap_homotopic line 553
  37. lemma OAI.Thomason.WeakHomotopy.componentsMap_comp line 573
  38. lemma OAI.Thomason.WeakHomotopy.componentsMap_id line 578
  39. lemma OAI.Thomason.WeakHomotopy.componentsMap_homotopic line 582
  40. theorem OAI.Thomason.WeakHomotopy.equivalence_of_strong_retract line 593
  41. lemma OAI.Thomason.NormalizedChains.simplexRank_of_after_lt line 643
  42. lemma OAI.Thomason.NormalizedChains.prepend_support line 668
  43. lemma OAI.Thomason.NormalizedChains.simplexAtom_rank line 683