OAI/Geometry/WeakMTW/Geodesics/MinimizerCompactness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.WeakMTW.minimizingDomain_closed line 22
2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.minimizingDomain_compact line 25
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.minimizing_vectors_near_unique line 36
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.injectivity_mem_interior_minimizing line 52
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.zero_mem_injectivity line 66
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.strict_radial_mem_injectivity line 69
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.injectivity_extend line 80
8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.injectivityDomain_open line 93