OAI/Combinatorics/IndependentSets/Reduction/ListIndex.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.ListIndex line 8
  2. abbrev OAI.LargeIndependentSets.ListSlot line 11
  3. abbrev OAI.LargeIndependentSets.EqualityData line 13
  4. def OAI.LargeIndependentSets.IsPattern line 15
  5. abbrev OAI.LargeIndependentSets.ListPattern line 22
  6. lemma OAI.LargeIndependentSets.isClosed_isPattern line 25
  7. instance OAI.LargeIndependentSets.(instance at line 72) line 72
  8. instance OAI.LargeIndependentSets.(instance at line 75) line 75
  9. instance OAI.LargeIndependentSets.(instance at line 78) line 78
  10. def OAI.LargeIndependentSets.ListIndex.map line 81
  11. def OAI.LargeIndependentSets.ListSlot.map line 85
  12. lemma OAI.LargeIndependentSets.ListIndex.map_injective line 88
  13. lemma OAI.LargeIndependentSets.ListSlot.map_injective line 94
  14. def OAI.LargeIndependentSets.ListPattern.restrict line 100
  15. lemma OAI.LargeIndependentSets.ListPattern.continuous_restrict line 115
  16. lemma OAI.LargeIndependentSets.ListIndex.min_map line 126
  17. lemma OAI.LargeIndependentSets.ListPattern.occupied_of_eq line 138
  18. lemma OAI.LargeIndependentSets.ListPattern.min_le_max line 142
  19. def OAI.LargeIndependentSets.patternCutValues line 153
  20. lemma OAI.LargeIndependentSets.patternCutValues_nonempty line 159
  21. lemma OAI.LargeIndependentSets.patternCutValues_bddAbove line 162
  22. def OAI.LargeIndependentSets.patternCut line 170
  23. lemma OAI.LargeIndependentSets.patternCut_le_iff line 173
  24. lemma OAI.LargeIndependentSets.patternCut_hull line 187
  25. lemma OAI.LargeIndependentSets.patternCut_eq_of_eq line 198
  26. lemma OAI.LargeIndependentSets.patternEval_continuous line 209
  27. lemma OAI.LargeIndependentSets.patternCut_measurable line 214
  28. def OAI.LargeIndependentSets.ListIndex.mapEquiv line 239
  29. def OAI.LargeIndependentSets.ListSlot.mapEquiv line 252
  30. lemma OAI.LargeIndependentSets.ListSlot.mapEquiv_apply line 256
  31. lemma OAI.LargeIndependentSets.patternCut_rat_iff line 260
  32. lemma OAI.LargeIndependentSets.patternCut_restrict_CDF line 267
  33. lemma OAI.LargeIndependentSets.ListSlot.map_eq_self line 294
  34. theorem OAI.LargeIndependentSets.invariant_cut_support_open line 311