OAI/Analysis/LipschitzEquivalence/FreeSpace.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.FreeSpace.lipZeroSubmodule line 16
  2. def OAI.LipschitzCounterexample.FreeSpace.LipZero line 26
  3. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 28) line 28
  4. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 29) line 29
  5. theorem OAI.LipschitzCounterexample.FreeSpace.apply_zero line 33
  6. def OAI.LipschitzCounterexample.FreeSpace.slopes line 35
  7. def OAI.LipschitzCounterexample.FreeSpace.slopesLinear line 48
  8. theorem OAI.LipschitzCounterexample.FreeSpace.slopes_injective line 65
  9. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 75) line 75
  10. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 78) line 78
  11. theorem OAI.LipschitzCounterexample.FreeSpace.norm_le_of_lipschitz line 81
  12. theorem OAI.LipschitzCounterexample.FreeSpace.norm_sub_le line 93
  13. theorem OAI.LipschitzCounterexample.FreeSpace.lipschitz line 102
  14. theorem OAI.LipschitzCounterexample.FreeSpace.norm_apply_le line 107
  15. def OAI.LipschitzCounterexample.FreeSpace.delta line 110
  16. theorem OAI.LipschitzCounterexample.FreeSpace.delta_apply line 116
  17. theorem OAI.LipschitzCounterexample.FreeSpace.delta_zero line 118
  18. theorem OAI.LipschitzCounterexample.FreeSpace.norm_delta_sub_le line 122
  19. def OAI.LipschitzCounterexample.FreeSpace.distanceTest line 127
  20. theorem OAI.LipschitzCounterexample.FreeSpace.norm_distanceTest_le line 135
  21. theorem OAI.LipschitzCounterexample.FreeSpace.norm_delta_sub line 142
  22. def OAI.LipschitzCounterexample.FreeSpace.freeSubmodule line 151
  23. def OAI.LipschitzCounterexample.FreeSpace.Space line 154
  24. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 156) line 156
  25. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 159) line 159
  26. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 162) line 162
  27. def OAI.LipschitzCounterexample.FreeSpace.point line 167
  28. theorem OAI.LipschitzCounterexample.FreeSpace.point_zero line 170
  29. theorem OAI.LipschitzCounterexample.FreeSpace.isometry_point line 174
  30. def OAI.LipschitzCounterexample.FreeSpace.inclusion line 180
  31. theorem OAI.LipschitzCounterexample.FreeSpace.dense_combinations line 186
  32. instance OAI.LipschitzCounterexample.FreeSpace.(instance at line 204) line 204
  33. def OAI.LipschitzCounterexample.FreeSpace.pullback line 214
  34. theorem OAI.LipschitzCounterexample.FreeSpace.norm_pullback_le line 218
  35. theorem OAI.LipschitzCounterexample.FreeSpace.combination_pairing line 224
  36. theorem OAI.LipschitzCounterexample.FreeSpace.norm_combination_le line 237
  37. def OAI.LipschitzCounterexample.FreeSpace.linearize line 254
  38. theorem OAI.LipschitzCounterexample.FreeSpace.linearize_point line 257
  39. theorem OAI.LipschitzCounterexample.FreeSpace.norm_linearize_le line 262
  40. theorem OAI.LipschitzCounterexample.FreeSpace.linearize_unique line 266
  41. theorem OAI.LipschitzCounterexample.FreeSpace.lipschitz_linearize line 284