OAI/Analysis/LipschitzEquivalence/GraphEmbedding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.Criterion.symm_zero line 21
  2. theorem OAI.LipschitzCounterexample.Criterion.Binv_zero line 27
  3. def OAI.LipschitzCounterexample.Criterion.graphEquiv line 30
  4. theorem OAI.LipschitzCounterexample.Criterion.lipschitz_graphEquiv line 46
  5. theorem OAI.LipschitzCounterexample.Criterion.lipschitz_graphEquiv_symm line 51
  6. def OAI.LipschitzCounterexample.Criterion.c0EmbedFun line 58
  7. theorem OAI.LipschitzCounterexample.Criterion.c0EmbedFun_coord line 78
  8. theorem OAI.LipschitzCounterexample.Criterion.norm_c0EmbedFun line 83
  9. def OAI.LipschitzCounterexample.Criterion.c0Embed line 114