OAI/Analysis/LipschitzEquivalence/CompactLipschitz.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.LocalLipschitz.disjoint_sum_lipschitz line 18
2. theorem OAI.LipschitzCounterexample.LocalLipschitz.compact_eventual_lipschitz line 66
3. def OAI.LipschitzCounterexample.LocalLipschitz.weightedRemainder line 105
4. theorem OAI.LipschitzCounterexample.LocalLipschitz.weightedRemainder_sub line 109
5. theorem OAI.LipschitzCounterexample.LocalLipschitz.weightedRemainder_lipschitzOn line 121
6. theorem OAI.LipschitzCounterexample.LocalGeometry.exists_disjoint_balls line 160