OAI/Combinatorics/ThinTrees/HierarchyBuilder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StrongThinTree.MultiGraph.Hierarchy.exists_structure line 14
2. structure OAI.StrongThinTree.MultiGraph.PartitionChain line 47
3. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.parts_nonempty line 54
4. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.parts_disjoint line 57
5. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.part_exists line 61
6. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.intersect_eq line 65
7. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.subset_of_intersect line 70
8. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.laminar line 78
9. def OAI.StrongThinTree.MultiGraph.PartitionChain.nodes line 88
10. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.mem_nodes line 91
11. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.nodes_nonempty line 102
12. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.nodes_laminar line 107
13. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.exists_hierarchy line 123
14. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.parent_at_transition line 131