OAI/Probability/MatroidProphet/Reverse/Paths.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.reversePrefix line 9
  2. def OAI.MatroidProphet.reverseNominal line 15
  3. lemma OAI.MatroidProphet.reversePrefix_succ line 19
  4. lemma OAI.MatroidProphet.reversePrefix_agrees line 24
  5. lemma OAI.MatroidProphet.reverseNominal_agrees line 34
  6. lemma OAI.MatroidProphet.reversePrefix_mono line 41
  7. lemma OAI.MatroidProphet.reverseNominal_mono line 52
  8. lemma OAI.MatroidProphet.reversePrefix_congr_before line 59
  9. lemma OAI.MatroidProphet.reverseNominal_congr_before line 69
  10. lemma OAI.MatroidProphet.reversePrefix_subset_later line 75
  11. lemma OAI.MatroidProphet.reverseNominal_subset_later line 89
  12. lemma OAI.MatroidProphet.reversePrefix_subset_succ line 96
  13. lemma OAI.MatroidProphet.union_inter_sdiff line 103
  14. def OAI.MatroidProphet.departingGuards line 108
  15. lemma OAI.MatroidProphet.reversePrefix_departing_only line 112
  16. lemma OAI.MatroidProphet.reverseNominal_departing_only line 127
  17. def OAI.MatroidProphet.departureBatch line 133
  18. lemma OAI.MatroidProphet.departureBatch_disjoint_time line 137
  19. lemma OAI.MatroidProphet.departureBatch_disjoint_group line 146
  20. def OAI.MatroidProphet.hybridGuards line 151
  21. def OAI.MatroidProphet.lowerCompetition line 156
  22. lemma OAI.MatroidProphet.hybridPrefix_contains line 162
  23. lemma OAI.MatroidProphet.hybrid_containment line 199