OAI/Probability/MatroidProphet/Pivots/GreedyScan.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.keptOccurrences line 13
2. lemma OAI.MatroidProphet.Pivots.mem_closure_kept_upto line 18
3. lemma OAI.MatroidProphet.Pivots.greedy_prefix_closure line 42
4. lemma OAI.MatroidProphet.Pivots.indep_image_of_notMem_prior line 57
5. lemma OAI.MatroidProphet.Pivots.keptOccurrences_indep line 90