OAI/Probability/MatroidProphet/Priority.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatroidProphet.levelWeight_mono line 8
  2. def OAI.MatroidProphet.Priority.asLevel line 23
  3. lemma OAI.MatroidProphet.Priority.asLevel_none line 25
  4. lemma OAI.MatroidProphet.Priority.asLevel_some line 26
  5. def OAI.MatroidProphet.Priority.Higher line 32
  6. def OAI.MatroidProphet.Priority.earlier line 35
  7. def OAI.MatroidProphet.Priority.time line 39
  8. lemma OAI.MatroidProphet.Priority.higher_trans line 41
  9. lemma OAI.MatroidProphet.Priority.higher_irrefl line 45
  10. lemma OAI.MatroidProphet.Priority.higher_total line 48
  11. lemma OAI.MatroidProphet.Priority.time_lt_of_higher line 52
  12. lemma OAI.MatroidProphet.Priority.time_lt_iff_higher line 66
  13. lemma OAI.MatroidProphet.Priority.time_injective line 78
  14. lemma OAI.MatroidProphet.Priority.time_lt_card line 87
  15. def OAI.MatroidProphet.Priority.timeEquiv line 97
  16. def OAI.MatroidProphet.Priority.order line 104
  17. lemma OAI.MatroidProphet.Priority.priorityTime_order line 106
  18. lemma OAI.MatroidProphet.Priority.main_higher_iff line 109
  19. lemma OAI.MatroidProphet.Priority.main_higher_iff_time line 115
  20. lemma OAI.MatroidProphet.Priority.higher_key_le line 119
  21. lemma OAI.MatroidProphet.Priority.order_antitone_levelWeight line 125
  22. lemma OAI.MatroidProphet.Priority.rounded_greedy_optimal line 138