OAI/Combinatorics/TreeEdit/CycleCharging.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TreeEdit.cycle_coordinates line 11
2. lemma OAI.TreeEdit.split_cycle_gap line 19
3. lemma OAI.TreeEdit.alignment_window_bound line 40
4. lemma OAI.TreeEdit.blockIndex_monotone line 82
5. lemma OAI.TreeEdit.card_block_fiber line 87
6. lemma OAI.TreeEdit.blockIndex_window line 108
7. lemma OAI.TreeEdit.sum_block_losses line 117
8. lemma OAI.TreeEdit.split_cycle_span_gap line 129
9. lemma OAI.TreeEdit.cycle_charging line 161