OAI/Analysis/LipschitzFree/WedgeApproximation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Compact-uniform approximation on wedges and contractive BAP inheritance

  1. theorem OAI.DiscreteFree.contraction_norm line 25
  2. theorem OAI.DiscreteFree.finiteRank_sandwich line 28
  3. theorem OAI.DiscreteFree.hasBAP_of_contractive_retract line 37
  4. def OAI.DiscreteFree.MetricWedge.inclusionL line 63
  5. def OAI.DiscreteFree.MetricWedge.retractionL line 67
  6. theorem OAI.DiscreteFree.MetricWedge.retractionL_inclusionL line 71
  7. theorem OAI.DiscreteFree.MetricWedge.inclusionL_bound line 77
  8. theorem OAI.DiscreteFree.MetricWedge.retractionL_bound line 78
  9. def OAI.DiscreteFree.MetricWedge.retainL line 80
  10. theorem OAI.DiscreteFree.MetricWedge.retainL_bound line 83
  11. theorem OAI.DiscreteFree.MetricWedge.retain_span_fixed line 85
  12. theorem OAI.DiscreteFree.MetricWedge.retain_error_bound line 110
  13. theorem OAI.DiscreteFree.MetricWedge.retain_pointwise line 117
  14. theorem OAI.DiscreteFree.MetricWedge.retain_compact line 127
  15. def OAI.DiscreteFree.MetricWedge.collapseL line 142
  16. def OAI.DiscreteFree.MetricWedge.embedL line 145
  17. theorem OAI.DiscreteFree.MetricWedge.embedL_bound line 148
  18. theorem OAI.DiscreteFree.MetricWedge.embedL_collapseL line 150
  19. theorem OAI.DiscreteFree.MetricWedge.hasAP line 156