OAI/Probability/MatroidProphet/Reverse/Iteration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatroidProphet.reversePrefix_flat line 12
  2. lemma OAI.MatroidProphet.reverseNominal_flat line 23
  3. lemma OAI.MatroidProphet.reversePrefix_into_output line 30
  4. lemma OAI.MatroidProphet.reverseNominal_into_output line 45
  5. def OAI.MatroidProphet.ReverseClosed line 52
  6. lemma OAI.MatroidProphet.reverseClosed_univ line 57
  7. def OAI.MatroidProphet.reverseStepTree line 61
  8. lemma OAI.MatroidProphet.reverseStepTree_run line 67
  9. lemma OAI.MatroidProphet.reverseStepTree_run_coordinate line 74
  10. lemma OAI.MatroidProphet.reverseStepTree_fresh line 82
  11. lemma OAI.MatroidProphet.reverseStepTree_queried line 90
  12. lemma OAI.MatroidProphet.reverseStepTree_closed line 96
  13. lemma OAI.MatroidProphet.reverseStepTree_remaining line 103
  14. def OAI.MatroidProphet.reverseTransactions line 118
  15. lemma OAI.MatroidProphet.reverseTransactions_fresh line 126