OAI/Probability/MatroidProphet/Pivots/BlockPatterns.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.blockLabel line 11
2. def OAI.MatroidProphet.Pivots.blockPrefix line 14
3. def OAI.MatroidProphet.Pivots.blockBefore line 17
4. def OAI.MatroidProphet.Pivots.blockBirthPattern line 20
5. lemma OAI.MatroidProphet.Pivots.pivot_block_birth line 26
6. lemma OAI.MatroidProphet.Pivots.block_birth_unique line 39
7. lemma OAI.MatroidProphet.Pivots.blockBirthPattern_mem_freeMarkedPatterns line 52
8. lemma OAI.MatroidProphet.Pivots.blockPrefix_eq line 78
9. lemma OAI.MatroidProphet.Pivots.blockBefore_eq_iUnion line 94