OAI/Combinatorics/ThinTrees/CompactPacking.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.StrongThinTree.MultiGraph.CompactPackage line 16
2. def OAI.StrongThinTree.MultiGraph.CompactPackage.mass line 23
3. lemma OAI.StrongThinTree.MultiGraph.CompactPackage.finite_bound line 25
4. lemma OAI.StrongThinTree.MultiGraph.CompactPackage.ordered_bound line 50
5. def OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedBag.weaken line 70
6. def OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedFamily.weaken line 76
7. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.mass_eq line 88
8. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.geometric_of_pairwise line 93
9. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.ratios_of_mem line 103
10. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.fresh_of_pairwise line 109
11. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.finite_bound line 119
12. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.AssignedSequence.ordered_bound line 136
13. abbrev OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily line 164
14. def OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.radius line 169
15. def OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.upper line 172
16. def OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.mass line 175
17. def OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.owners line 178
18. def OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.Ratio line 182
19. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.mass_nonneg line 187
20. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.mixed_bound line 192
21. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.CapturedFamily.scale_bound line 268
22. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.capturePackage line 321
23. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.homogeneous_scale_bound line 368