OAI/Probability/MatroidProphet/Pivots/Basic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.support line 12
2. lemma OAI.MatroidProphet.Pivots.support_subset line 15
3. lemma OAI.MatroidProphet.Pivots.support_subset_of_mem_closure line 18
4. lemma OAI.MatroidProphet.Pivots.mem_closure_support line 22
5. lemma OAI.MatroidProphet.Pivots.mem_closure_iff_support_subset line 29
6. lemma OAI.MatroidProphet.Pivots.support_nonempty line 37
7. lemma OAI.MatroidProphet.Pivots.support_unique line 44
8. lemma OAI.MatroidProphet.Pivots.old_redundant_after_insertions line 51
9. lemma OAI.MatroidProphet.Pivots.mem_closure_prefix_iff line 56