OAI/Analysis/LipschitzEquivalence/InverseTails.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.HilbertSlots.cutHead line 15
  2. theorem OAI.LipschitzCounterexample.HilbertSlots.prefix_tendsto line 18
  3. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_sub_prefix_sq line 21
  4. theorem OAI.LipschitzCounterexample.HilbertSlots.cauchy_of_small_tails line 26
  5. theorem OAI.LipschitzCounterexample.HilbertSlots.subsequence_of_tail_domination line 49
  6. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_tail_norm_sq line 81
  7. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_fst_tail line 92
  8. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_snd_tail line 100
  9. theorem OAI.LipschitzCounterexample.HilbertSlots.inverse_subsequence line 110
  10. def OAI.LipschitzCounterexample.GlobalInverse.uniqueFiber line 135
  11. theorem OAI.LipschitzCounterexample.GlobalInverse.uniqueFiber_iff line 139
  12. theorem OAI.LipschitzCounterexample.GlobalInverse.covering_bijective line 147
  13. theorem OAI.LipschitzCounterexample.GlobalInverse.proper_covering line 183
  14. theorem OAI.LipschitzCounterexample.GlobalInverse.proper_of_norm line 200
  15. theorem OAI.LipschitzCounterexample.GlobalInverse.norm_local_bijective line 210
  16. theorem OAI.LipschitzCounterexample.HilbertSlots.moving_limit_surjective line 225