OAI/Probability/MatroidProphet/Pivots/Blocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatroidProphet.Pivots.BlockOld line 13
2. instance OAI.MatroidProphet.Pivots.(instance at line 16) line 16
3. def OAI.MatroidProphet.Pivots.blockOldStage line 18
4. def OAI.MatroidProphet.Pivots.blockOldLabel line 20
5. def OAI.MatroidProphet.Pivots.blockStage line 22
6. def OAI.MatroidProphet.Pivots.blockKey line 25
7. lemma OAI.MatroidProphet.Pivots.blockKey_injective line 30
8. def OAI.MatroidProphet.Pivots.blockTime line 61
9. lemma OAI.MatroidProphet.Pivots.blockTime_lt_iff line 65
10. lemma OAI.MatroidProphet.Pivots.blockTime_injective line 72
11. lemma OAI.MatroidProphet.Pivots.blockTime_old_strictMono line 80
12. lemma OAI.MatroidProphet.Pivots.stage_lt_implies_blockTime_lt line 92
13. lemma OAI.MatroidProphet.Pivots.blockTime_le_implies_stage_le line 100