OAI/Analysis/BiholderTransport/Geodesics/InjectivityOpen.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.interior_minimizingVectors_subset line 93
2. lemma OAI.WeakMTWTransport.injectivityDomain_subset_interior_minimizingVectors line 115
3. lemma OAI.WeakMTWTransport.injectivityDomain_eq_interior_minimizingVectors line 140
4. lemma OAI.WeakMTWTransport.isOpen_injectivityDomain line 145