OAI/Probability/MatroidProphet/Pivots/Greedy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.oldPrefix line 12
2. lemma OAI.MatroidProphet.Pivots.oldPrefix_zero line 14
3. lemma OAI.MatroidProphet.Pivots.oldPrefix_succ line 19
4. lemma OAI.MatroidProphet.Pivots.oldPrefix_mono line 32
5. lemma OAI.MatroidProphet.Pivots.conditionalRank_singleton_of_notMem_closure line 38
6. lemma OAI.MatroidProphet.Pivots.conditionalRank_singleton_of_mem_closure line 46
7. def OAI.MatroidProphet.Pivots.omittable line 54
8. lemma OAI.MatroidProphet.Pivots.omittable_drop line 58
9. lemma OAI.MatroidProphet.Pivots.card_omittable_le_rank line 69
10. lemma OAI.MatroidProphet.Pivots.notMem_closure_before_nonomittable line 99
11. def OAI.MatroidProphet.Pivots.vulnerable line 110
12. lemma OAI.MatroidProphet.Pivots.card_vulnerable_le_rank line 115