OAI/Probability/MatroidProphet/Pivots/Interleavings.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatroidProphet.Pivots.Occurrence line 13
2. def OAI.MatroidProphet.Pivots.occurrenceLabel line 15
3. def OAI.MatroidProphet.Pivots.OldOrdered line 18
4. def OAI.MatroidProphet.Pivots.retained line 21
5. def OAI.MatroidProphet.Pivots.retainedFamily line 27
6. lemma OAI.MatroidProphet.Pivots.before_old_subset line 32
7. lemma OAI.MatroidProphet.Pivots.retains_nonomittable_old line 49
8. lemma OAI.MatroidProphet.Pivots.card_retainedFamily_le line 59