OAI/Analysis/HardSphere/Conditioning/SlotMultiplicity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.nearSlots_card_of_fiber line 14
2. lemma OAI.HardSphere.Comparison.departure_anchor_injective line 37
3. lemma OAI.HardSphere.Comparison.routeSlots_start_fiber line 47
4. lemma OAI.HardSphere.Comparison.routeSlots_start_sites line 91
5. lemma OAI.HardSphere.Comparison.second_primary_nearSlots_bound line 105