OAI/Combinatorics/ThinTrees/ChainEdges.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrongThinTree.MultiGraph.PartitionChain.block line 12
2. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.block_mem line 13
3. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.mem_block line 14
4. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.block_eq_of_mem line 15
5. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.block_subset line 17
6. def OAI.StrongThinTree.MultiGraph.PartitionChain.crossing line 21
7. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.mem_crossing line 22
8. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.crossing_antitone line 24
9. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.crossing_root line 31
10. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.cut_part_crossing line 38
11. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.boundary_sum_le line 50
12. lemma OAI.StrongThinTree.MultiGraph.PartitionChain.disappearing_in_parentBoundary line 80