OAI/Probability/MatroidProphet/Pivots/ResidualFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.smallSubsets line 13
2. lemma OAI.MatroidProphet.Pivots.mem_smallSubsets line 17
3. lemma OAI.MatroidProphet.Pivots.card_smallSubsets_le line 23
4. def OAI.MatroidProphet.Pivots.intersectionFamily line 35
5. lemma OAI.MatroidProphet.Pivots.card_intersectionFamily_le line 38
6. def OAI.MatroidProphet.Pivots.residualFamily line 42
7. lemma OAI.MatroidProphet.Pivots.mem_residualFamily line 51
8. lemma OAI.MatroidProphet.Pivots.card_residualFamily_le line 65
9. lemma OAI.MatroidProphet.Pivots.card_residualFamily_le_exp line 115