OAI/CategoryTheory/Thomason/LayeredWhiskers.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Layered Whiskers.

  1. lemma OAI.Thomason.OmegaCategory.join_distribute_left line 16
  2. lemma OAI.Thomason.OmegaCategory.join_distribute_right line 32
  3. def OAI.Thomason.OmegaCategory.LayeredWhisker line 48
  4. lemma OAI.Thomason.OmegaCategory.LayeredWhisker.of_generator line 59
  5. lemma OAI.Thomason.OmegaCategory.LayeredWhisker.left line 71
  6. lemma OAI.Thomason.OmegaCategory.LayeredWhisker.right line 129
  7. theorem OAI.Thomason.OmegaCategory.Whisker.layered line 183
  8. lemma OAI.Thomason.DirectedComplex.Table.comp_left_cancel line 203
  9. lemma OAI.Thomason.DirectedComplex.Table.comp_right_cancel line 220
  10. lemma OAI.Thomason.DirectedComplex.Table.join_left_cancel line 237
  11. lemma OAI.Thomason.DirectedComplex.Table.join_right_cancel line 244
  12. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_and_target_ext line 258
  13. def OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker line 283
  14. lemma OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.layered line 296
  15. lemma OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.row_above line 304
  16. lemma OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.of_atom line 326
  17. lemma OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.split_unique line 345
  18. theorem OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.eq_of_map_eq line 365
  19. lemma OAI.Thomason.DirectedComplex.Table.factor_context_with_top line 440
  20. theorem OAI.Thomason.DirectedComplex.RankedAtoms.table_ordered_whisker line 520
  21. theorem OAI.Thomason.DirectedComplex.RankedAtoms.OrderedWhisker.lift line 598
  22. theorem OAI.Thomason.DirectedComplex.RankedAtoms.unique_ordered_lift line 642
  23. lemma OAI.Thomason.OmegaCategory.Functor.bounded_ext line 672
  24. lemma OAI.Thomason.OmegaCategory.LayeredWhisker.row_bounded line 677
  25. lemma OAI.Thomason.OmegaCategory.LayeredWhisker.whisker line 690