OAI/Analysis/BiholderTransport/Coordinates/ExpNonconjugacy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.riemannianExp_interior_nonconjugate line 84
2. lemma OAI.WeakMTWTransport.contMDiff_riemannianExp_fiber line 107
3. lemma OAI.WeakMTWTransport.exists_coordinate_exp_inverse line 115
4. lemma OAI.WeakMTWTransport.riemannianExp_locally_injective line 148