OAI/Analysis/LipschitzEquivalence/LocalLipschitz.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.LocalLipschitz.quotients line 18
  2. def OAI.LipschitzCounterexample.LocalLipschitz.constant line 21
  3. theorem OAI.LipschitzCounterexample.LocalLipschitz.quotients_nonempty line 23
  4. theorem OAI.LipschitzCounterexample.LocalLipschitz.quotient_le line 26
  5. theorem OAI.LipschitzCounterexample.LocalLipschitz.quotients_bounded line 33
  6. theorem OAI.LipschitzCounterexample.LocalLipschitz.constant_nonneg line 40
  7. theorem OAI.LipschitzCounterexample.LocalLipschitz.constant_le line 44
  8. theorem OAI.LipschitzCounterexample.LocalLipschitz.lipschitzOn_constant line 51
  9. theorem OAI.LipschitzCounterexample.LocalLipschitz.subsequence_constants line 61
  10. theorem OAI.LipschitzCounterexample.LocalLipschitz.uniform_zero_on_compact line 80
  11. theorem OAI.LipschitzCounterexample.LocalGeometry.scalar_local_lipschitz line 114
  12. def OAI.LipschitzCounterexample.LocalGeometry.LocalOrthogonality line 144
  13. def OAI.LipschitzCounterexample.LocalGeometry.badSet line 155
  14. theorem OAI.LipschitzCounterexample.LocalGeometry.badSet_finite line 158