OAI/Analysis/BiholderTransport/Coordinates/FiberwiseHomeomorphism.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.fiberwiseHomeomorph line 73
2. lemma OAI.WeakMTWTransport.fiberwiseHomeomorph_contDiffOn line 115
3. lemma OAI.WeakMTWTransport.fiberwiseHomeomorph_symm_contDiffOn line 122
4. lemma OAI.WeakMTWTransport.first_coordinate_preserving_derivative_invertible line 131