OAI/Analysis/HardSphere/Bridges/TorusLocalBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.localLiftChart line 15
2. lemma OAI.HardSphere.localLiftChart_preserving line 18
3. lemma OAI.HardSphere.project_injOn_chart line 33
4. lemma OAI.HardSphere.ball_subset_localLiftChart line 40
5. lemma OAI.HardSphere.isOpenMap_project line 48
6. lemma OAI.HardSphere.project_ball_preserving line 57
7. lemma OAI.HardSphere.killed_ae_torus_local_pairs line 73