OAI/CategoryTheory/Thomason/RankedExchange.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Ranked Exchange.

  1. inductive OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath line 18
  2. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.bounded line 29
  3. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.topSequence line 36
  4. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.append line 42
  5. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.single line 58
  6. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.coefficient line 68
  7. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.nodup line 83
  8. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.perm_of_image_eq line 92
  9. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.dim_of_mem line 102
  10. lemma OAI.Thomason.DirectedComplex.RankedAtoms.topSequence_path line 113
  11. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_atom_path line 136
  12. def OAI.Thomason.DirectedComplex.RankedAtoms.orderRank line 158
  13. lemma OAI.Thomason.DirectedComplex.RankedAtoms.orderRank_strict line 161
  14. lemma OAI.Thomason.DirectedComplex.RankedAtoms.orderRank_injective line 171
  15. lemma OAI.Thomason.DirectedComplex.RankedAtoms.rank_le_of_orderRank_le line 183
  16. lemma OAI.Thomason.DirectedComplex.RankedAtoms.table_topSequence line 188
  17. lemma OAI.Thomason.DirectedComplex.RankedAtoms.table_single_whisker line 200
  18. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.mass line 210
  19. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.sorted_list_unique line 220
  20. theorem OAI.Thomason.DirectedComplex.RankedAtoms.table_sorted_atomPath line 233
  21. def OAI.Thomason.DirectedComplex.RankedAtoms.WhiskerFaithful line 316
  22. def OAI.Thomason.DirectedComplex.RankedAtoms.HasAdjacentExchange line 320
  23. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.eq_of_same_list line 338
  24. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.eq_of_sorted line 375
  25. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.insert_sorted line 387
  26. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.sorted line 444
  27. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.eq_of_exchange line 454
  28. lemma OAI.Thomason.DirectedComplex.RankedAtoms.onCells_injective_of_exchange line 466
  29. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.of_single line 496
  30. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.nil_bounded line 506
  31. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.view_cons line 510
  32. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.singleton_data line 519
  33. lemma OAI.Thomason.DirectedComplex.RankedAtoms.table_whiskerFaithful line 528
  34. lemma OAI.Thomason.DirectedComplex.RankedAtoms.table_hasAdjacentExchange line 532
  35. def OAI.Thomason.DirectedComplex.RankedAtoms.TwoAtomFaithful line 561
  36. lemma OAI.Thomason.DirectedComplex.RankedAtoms.whiskerFaithful_of_twoAtomFaithful line 565
  37. lemma OAI.Thomason.DirectedComplex.RankedAtoms.hasAdjacentExchange_of_twoAtomFaithful line 574
  38. lemma OAI.Thomason.DirectedComplex.RankedAtoms.onCells_injective_of_twoAtomFaithful line 624
  39. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_onCells_injective_of_twoAtomFaithful line 644
  40. def OAI.Thomason.GrayRecursive.IntervalHom.finLiftOrderIso line 669
  41. def OAI.Thomason.GrayRecursive.IntervalHom.standardPrismBasis line 673
  42. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standard_twoAtomFaithful line 677
  43. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_onCells_injective_of_local_exchange line 693
  44. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standard_local_exchange line 711