OAI/Analysis/LipschitzEquivalence/GraphEquivalence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LipschitzCounterexample.Criterion.Domain line 16
  2. abbrev OAI.LipschitzCounterexample.Criterion.Free line 17
  3. abbrev OAI.LipschitzCounterexample.Criterion.Sum line 19
  4. def OAI.LipschitzCounterexample.Criterion.Q1 line 24
  5. theorem OAI.LipschitzCounterexample.Criterion.Q1_fst line 28
  6. theorem OAI.LipschitzCounterexample.Criterion.Q1_snd line 29
  7. theorem OAI.LipschitzCounterexample.Criterion.norm_Q1_le line 31
  8. theorem OAI.LipschitzCounterexample.Criterion.lipschitz_Q1 line 48
  9. def OAI.LipschitzCounterexample.Criterion.B line 54
  10. theorem OAI.LipschitzCounterexample.Criterion.B_zero line 56
  11. theorem OAI.LipschitzCounterexample.Criterion.lipschitz_B line 58
  12. theorem OAI.LipschitzCounterexample.Criterion.diagram line 80
  13. def OAI.LipschitzCounterexample.Criterion.Binv line 84
  14. theorem OAI.LipschitzCounterexample.Criterion.Q1_Binv line 88
  15. theorem OAI.LipschitzCounterexample.Criterion.B_Binv line 97
  16. theorem OAI.LipschitzCounterexample.Criterion.Binv_B line 103
  17. def OAI.LipschitzCounterexample.Criterion.diagramEquiv line 112
  18. theorem OAI.LipschitzCounterexample.Criterion.lipschitz_Binv line 119