OAI/Analysis/LipschitzEquivalence/NullSequences.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LipschitzCounterexample.NullSequences.C0 line 16
  2. def OAI.LipschitzCounterexample.NullSequences.ofTendsto line 18
  3. theorem OAI.LipschitzCounterexample.NullSequences.tendsto_zero line 23
  4. theorem OAI.LipschitzCounterexample.NullSequences.norm_apply_le line 26
  5. theorem OAI.LipschitzCounterexample.NullSequences.norm_le line 29
  6. def OAI.LipschitzCounterexample.NullSequences.evalAddHom line 33
  7. theorem OAI.LipschitzCounterexample.NullSequences.sum_apply line 38
  8. def OAI.LipschitzCounterexample.NullSequences.single line 41
  9. theorem OAI.LipschitzCounterexample.NullSequences.single_apply line 47
  10. theorem OAI.LipschitzCounterexample.NullSequences.single_zero line 50
  11. theorem OAI.LipschitzCounterexample.NullSequences.single_sub line 54
  12. theorem OAI.LipschitzCounterexample.NullSequences.norm_single line 59
  13. theorem OAI.LipschitzCounterexample.NullSequences.isometry_single line 66
  14. def OAI.LipschitzCounterexample.NullSequences.trunc line 71
  15. theorem OAI.LipschitzCounterexample.NullSequences.trunc_apply line 74
  16. theorem OAI.LipschitzCounterexample.NullSequences.norm_sub_trunc_le line 78
  17. theorem OAI.LipschitzCounterexample.NullSequences.tendsto_trunc line 86
  18. def OAI.LipschitzCounterexample.NullSequences.evalCLM line 101
  19. instance OAI.LipschitzCounterexample.NullSequences.(instance at line 107) line 107