OAI/Analysis/LipschitzEquivalence/Multipliers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.FreeSpace.multiplier line 20
  2. theorem OAI.LipschitzCounterexample.FreeSpace.multiplier_lipschitz line 23
  3. theorem OAI.LipschitzCounterexample.FreeSpace.multiplier_point line 33
  4. theorem OAI.LipschitzCounterexample.FreeSpace.norm_multiplier_le line 39
  5. theorem OAI.LipschitzCounterexample.FreeSpace.supported_map line 45
  6. theorem OAI.LipschitzCounterexample.FreeSpace.supported_univ line 56
  7. theorem OAI.LipschitzCounterexample.FreeSpace.multiplier_supported line 66
  8. theorem OAI.LipschitzCounterexample.FreeSpace.multiplier_identity_on line 78
  9. def OAI.LipschitzCounterexample.FreeSpace.Approximable line 97
  10. theorem OAI.LipschitzCounterexample.FreeSpace.supported_mono line 100
  11. theorem OAI.LipschitzCounterexample.FreeSpace.Approximable.mono line 103
  12. theorem OAI.LipschitzCounterexample.FreeSpace.finite_bounded line 108
  13. theorem OAI.LipschitzCounterexample.FreeSpace.exists_radius_approx line 115
  14. theorem OAI.LipschitzCounterexample.FreeSpace.prefix_radius_approx line 122
  15. theorem OAI.LipschitzCounterexample.FreeSpace.test_eq_of_agree line 137
  16. theorem OAI.LipschitzCounterexample.FreeSpace.pairing_difference_le line 148