OAI/Analysis/HardSphere/Conditioning/RoutePartition.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.nearSlots line 15
2. def OAI.HardSphere.Comparison.farSlots line 17
3. lemma OAI.HardSphere.Comparison.mem_nearSlots line 20
4. lemma OAI.HardSphere.Comparison.mem_farSlots line 22
5. lemma OAI.HardSphere.Comparison.far_union_near line 25
6. lemma OAI.HardSphere.Comparison.far_near_disjoint line 29
7. lemma OAI.HardSphere.Comparison.far_other_disjoint line 31
8. lemma OAI.HardSphere.Comparison.far_partition_disjoint line 36
9. lemma OAI.HardSphere.Comparison.route_partition_union line 48
10. lemma OAI.HardSphere.Comparison.nearSlots_card line 52
11. lemma OAI.HardSphere.Comparison.commonSlots_near line 65
12. lemma OAI.HardSphere.Comparison.physical_far_slots line 73
13. def OAI.HardSphere.Comparison.routeEmbedding line 91
14. lemma OAI.HardSphere.Comparison.routeEmbedding_castSucc line 104
15. lemma OAI.HardSphere.Comparison.routeEmbedding_last line 108
16. def OAI.HardSphere.Comparison.routePermutation line 113
17. def OAI.HardSphere.Comparison.routeSlots line 116
18. lemma OAI.HardSphere.Comparison.routePermutation_fixed line 118
19. lemma OAI.HardSphere.Comparison.routePermutation_label line 125
20. lemma OAI.HardSphere.Comparison.routePermutation_star line 133
21. lemma OAI.HardSphere.Comparison.routePermutation_lastLabel line 140
22. lemma OAI.HardSphere.Comparison.routeSlots_exact line 145