OAI/Combinatorics/RamseyFive/Trees/TreeOrder.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.TreeCodec.Ordered line 11
2. lemma OAI.SharpRamseyFive.TreeCodec.label_mem_inorder line 17
3. lemma OAI.SharpRamseyFive.TreeCodec.exists_address_of_mem line 27
4. lemma OAI.SharpRamseyFive.TreeCodec.ordered_pathBudget_bound line 40
5. lemma OAI.SharpRamseyFive.TreeCodec.label_map_mem line 68
6. lemma OAI.SharpRamseyFive.TreeCodec.ordered_map line 80
7. lemma OAI.SharpRamseyFive.TreeCodec.map_height line 96
8. lemma OAI.SharpRamseyFive.TreeCodec.map_nodes line 102
9. lemma OAI.SharpRamseyFive.PivotTree.balanced_label_bounds line 110
10. lemma OAI.SharpRamseyFive.PivotTree.balanced_ordered line 117
11. def OAI.SharpRamseyFive.PivotTree.finiteBalanced line 132
12. lemma OAI.SharpRamseyFive.PivotTree.finiteBalanced_ordered line 135
13. lemma OAI.SharpRamseyFive.PivotTree.finiteBalanced_height line 140
14. lemma OAI.SharpRamseyFive.PivotTree.finiteBalanced_nodes line 144
15. lemma OAI.SharpRamseyFive.PivotTree.finiteBalanced_label_lt line 147