OAI/Analysis/LipschitzFree/Functor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Contractive linearization of pointed Lipschitz maps

  1. def OAI.DiscreteFree.lipPullback line 16
  2. theorem OAI.DiscreteFree.lipPullback_apply line 31
  3. theorem OAI.DiscreteFree.lipPullback_bound line 35
  4. theorem OAI.DiscreteFree.pullback_mem_free line 45
  5. def OAI.DiscreteFree.freeMap line 59
  6. theorem OAI.DiscreteFree.freeMap_delta line 72
  7. theorem OAI.DiscreteFree.freeMap_bound line 76
  8. theorem OAI.DiscreteFree.freeMap_ext line 86