OAI/Analysis/C0Absorption/Aharoni.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.earlierCut line 17
  2. theorem OAI.C0Absorption.earlierCut_le_scale line 21
  3. theorem OAI.C0Absorption.earlierCut_le_point line 26
  4. theorem OAI.C0Absorption.le_earlierCut line 35
  5. theorem OAI.C0Absorption.earlierCut_lipschitz line 41
  6. def OAI.C0Absorption.metricBump line 49
  7. theorem OAI.C0Absorption.metricBump_nonneg line 52
  8. theorem OAI.C0Absorption.metricBump_le_scale line 54
  9. theorem OAI.C0Absorption.metricBump_zero_of_far line 57
  10. theorem OAI.C0Absorption.metricBump_zero_of_base line 61
  11. theorem OAI.C0Absorption.metricBump_lipschitz line 65
  12. theorem OAI.C0Absorption.metricBump_eventually_zero line 74
  13. def OAI.C0Absorption.dyadicBump line 82
  14. theorem OAI.C0Absorption.dyadicBump_nonneg line 84
  15. theorem OAI.C0Absorption.dyadicBump_finite_large line 87
  16. theorem OAI.C0Absorption.dyadicBump_tendsto line 116
  17. def OAI.C0Absorption.dyadicC0 line 124
  18. theorem OAI.C0Absorption.dyadicC0_apply line 127
  19. theorem OAI.C0Absorption.dyadicC0_upper line 130
  20. theorem OAI.C0Absorption.dyadicBump_separates line 150
  21. theorem OAI.C0Absorption.dyadicC0_lower line 178
  22. theorem OAI.C0Absorption.cfunPull_dist_eq_of_surjective line 209
  23. def OAI.C0Absorption.dyadicEnumeration line 227
  24. def OAI.C0Absorption.aharoniEmbedding line 229
  25. theorem OAI.C0Absorption.aharoniEmbedding_dist line 232
  26. theorem OAI.C0Absorption.aharoniEmbedding_bilip line 236
  27. theorem OAI.C0Absorption.c0_metricUniversal line 243