OAI/Probability/MatroidProphet/Pivots/Arbitrary.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MatroidProphet.Pivots.oldPrefix_subset_beforeline 12 - lemma
OAI.MatroidProphet.Pivots.retained_old_initially_nonredundantline 20 - lemma
OAI.MatroidProphet.Pivots.card_retainedFamily_arbitrary_oldline 29