OAI/Probability/FreeIsing/Trees/PathPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.TreeAut.length_le_of_root_eq line 11
2. theorem OAI.Problem367.TreeAut.length_eq_of_root_eq line 37
3. theorem OAI.Problem367.TreeAut.root_eq_of_length_preserving line 49
4. theorem OAI.Problem367.TreeAut.symm_length_eq line 56
5. theorem OAI.Problem367.TreeAut.map_takeVertex_of_length_preserving line 61
6. theorem OAI.Problem367.TreeAut.map_prefixes_of_map_endpoint line 93
7. theorem OAI.Problem367.TreeAut.map_takeVertex_of_root_eq line 99
8. theorem OAI.Problem367.TreeAut.map_prefix_iff_of_length_preserving line 106