OAI/Analysis/LipschitzFree/Model.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Real Lipschitz-free spaces and compact-uniform approximation properties

  1. def OAI.DiscreteFree.lipSubmodule line 17

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:16 (same declaration text).

  2. def OAI.DiscreteFree.Lip0 line 45

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:44 (same declaration text).

  3. instance OAI.DiscreteFree.Lip0.(instance at line 51) line 51
  4. instance OAI.DiscreteFree.Lip0.(instance at line 52) line 52
  5. instance OAI.DiscreteFree.Lip0.(instance at line 54) line 54
  6. theorem OAI.DiscreteFree.Lip0.at_base line 56
  7. theorem OAI.DiscreteFree.Lip0.quotients_bounded line 58
  8. def OAI.DiscreteFree.Lip0.slope line 70

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:55 (same declaration text).

  9. theorem OAI.DiscreteFree.Lip0.slope_injective line 94
  10. instance OAI.DiscreteFree.Lip0.(instance at line 105) line 105
  11. instance OAI.DiscreteFree.Lip0.(instance at line 117) line 117
  12. theorem OAI.DiscreteFree.Lip0.norm_slope line 120
  13. theorem OAI.DiscreteFree.Lip0.norm_le_iff line 122
  14. theorem OAI.DiscreteFree.Lip0.sub_le line 141
  15. theorem OAI.DiscreteFree.Lip0.apply_le line 145
  16. def OAI.DiscreteFree.Lip0.ofBound line 148
  17. def OAI.DiscreteFree.evaluation line 154

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:96 (same declaration text).

  18. theorem OAI.DiscreteFree.evaluation_apply line 170
  19. theorem OAI.DiscreteFree.evaluation_base line 172
  20. def OAI.DiscreteFree.freeSubmodule line 176

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:112 (same declaration text).

  21. def OAI.DiscreteFree.FreeSpace line 179

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:115 (same declaration text).

  22. instance OAI.DiscreteFree.(instance at line 181) line 181
  23. instance OAI.DiscreteFree.(instance at line 184) line 184
  24. def OAI.DiscreteFree.delta line 187

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:123 (same declaration text).

  25. def OAI.DiscreteFree.HasAP line 191

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:127 (same declaration text).

  26. def OAI.DiscreteFree.BlockStatement line 196

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:139 (same declaration text).

  27. def OAI.DiscreteFree.MainStatement line 205

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:148 (same declaration text).