OAI/Combinatorics/VariableWL/Subdivision.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.VariableWL.Subdivision.Vertex line 11
2. abbrev OAI.VariableWL.Subdivision.Link line 12
3. def OAI.VariableWL.Subdivision.left line 14
4. def OAI.VariableWL.Subdivision.right line 18
5. theorem OAI.VariableWL.Subdivision.endpoints_ne line 22
6. theorem OAI.VariableWL.Subdivision.exists_unused_cut line 35
7. def OAI.VariableWL.Subdivision.owner line 51
8. theorem OAI.VariableWL.Subdivision.owner_real line 55
9. theorem OAI.VariableWL.Subdivision.owner_link line 58
10. def OAI.VariableWL.Subdivision.depth line 73
11. theorem OAI.VariableWL.Subdivision.depth_link line 77
12. def OAI.VariableWL.Subdivision.supportGraph line 89
13. theorem OAI.VariableWL.Subdivision.owner_adj line 101
14. theorem OAI.VariableWL.Subdivision.owner_walk line 110
15. theorem OAI.VariableWL.Subdivision.at_most_one_real line 118
16. def OAI.VariableWL.Subdivision.parent line 131
17. theorem OAI.VariableWL.Subdivision.parent_link line 141
18. theorem OAI.VariableWL.Subdivision.acyclic_of_unique_lower line 154
19. theorem OAI.VariableWL.Subdivision.chosen_support_acyclic line 181
20. theorem OAI.VariableWL.Subdivision.small_support_acyclic line 207
21. theorem OAI.VariableWL.Subdivision.internal_adj_wire line 214
22. theorem OAI.VariableWL.Markers.walkSum_congr line 230
23. theorem OAI.VariableWL.Markers.walkSum_zero line 237
24. theorem OAI.VariableWL.Markers.walkSum_add line 243
25. theorem OAI.VariableWL.Markers.walkSum_mul line 249