OAI/Combinatorics/Chromatic/Histories/SortedFiberPerm.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.Packets.fiber line 12
  2. def OAI.ElementaryPositivity.Packets.card line 13
  3. lemma OAI.ElementaryPositivity.Packets.mem_fiber line 14
  4. lemma OAI.ElementaryPositivity.Packets.card_eq line 15
  5. def OAI.ElementaryPositivity.Packets.fiberOrder line 17
  6. def OAI.ElementaryPositivity.Packets.fiberIso line 21
  7. def OAI.ElementaryPositivity.Packets.sortedPerm line 25
  8. lemma OAI.ElementaryPositivity.Packets.sortedPerm_map line 27
  9. def OAI.ElementaryPositivity.Packets.Sorted line 30
  10. lemma OAI.ElementaryPositivity.Packets.sortedPerm_sorted line 32
  11. lemma OAI.ElementaryPositivity.Packets.sorted_unique line 49
  12. lemma OAI.ElementaryPositivity.Packets.card_of_perm line 66
  13. def OAI.ElementaryPositivity.Packets.left line 82
  14. def OAI.ElementaryPositivity.Packets.right line 83
  15. def OAI.ElementaryPositivity.Packets.ascentMask line 84
  16. lemma OAI.ElementaryPositivity.Packets.mem_ascentMask line 86
  17. def OAI.ElementaryPositivity.Packets.gap line 89
  18. def OAI.ElementaryPositivity.Packets.indexVal line 90
  19. lemma OAI.ElementaryPositivity.Packets.indexVal_succ line 91
  20. lemma OAI.ElementaryPositivity.Packets.indexVal_mono line 93
  21. lemma OAI.ElementaryPositivity.Packets.indexVal_le line 98
  22. def OAI.ElementaryPositivity.Packets.index line 103
  23. lemma OAI.ElementaryPositivity.Packets.index_mono line 105
  24. lemma OAI.ElementaryPositivity.Packets.index_adjacent line 108
  25. lemma OAI.ElementaryPositivity.Packets.index_left_right line 123
  26. lemma OAI.ElementaryPositivity.Packets.inside_of_required line 127