OAI/Analysis/LipschitzEquivalence/GlobalInverse.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.GlobalInverse.proper_finite_perturbation line 15
2. theorem OAI.LipschitzCounterexample.GlobalInverse.finite_perturbation_bijective line 33
3. theorem OAI.LipschitzCounterexample.GlobalInverse.bijective_of_close_isometry line 41
4. theorem OAI.LipschitzCounterexample.GlobalInverse.derivative_bounds line 68
5. def OAI.LipschitzCounterexample.GlobalInverse.derivativeEquiv line 80
6. theorem OAI.LipschitzCounterexample.GlobalInverse.derivativeEquiv_apply line 86
7. theorem OAI.LipschitzCounterexample.GlobalInverse.localHomeomorph_of_deriv_close line 90
8. theorem OAI.LipschitzCounterexample.GlobalInverse.global_bounds_of_deriv_close line 98