OAI/Analysis/HardSphere/Bridges/RouteAuxiliary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Bridge.fiberEquiv_map line 18
2. lemma OAI.HardSphere.Bridge.reverseFactor_fst line 24
3. lemma OAI.HardSphere.Bridge.exists_two_auxiliary line 32
4. def OAI.HardSphere.Bridge.extendSelectedPair line 62
5. lemma OAI.HardSphere.Bridge.extendSelectedPair_selected line 68
6. instance OAI.HardSphere.Bridge.extendSelectedPair_probability line 73
7. lemma OAI.HardSphere.Bridge.extendSelectedPair_bounds line 81