OAI/Analysis/BiholderTransport/Coordinates/ManifoldLipschitz.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.contMDiffAt_exists_lipschitzOn line 23
2. lemma OAI.WeakMTWTransport.contMDiffOn_exists_lipschitzOn_compact line 45
3. lemma OAI.WeakMTWTransport.movingNormal_trivialization_exp line 62
4. lemma OAI.WeakMTWTransport.exp_lipschitz_near_base line 79
5. lemma OAI.WeakMTWTransport.exists_uniform_exp_lipschitz line 121