OAI/Analysis/LipschitzFree/RetainedWedge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Separated metric wedges and bounded finite-component retracts

  1. theorem OAI.DiscreteFree.MetricWedge.separated line 18
  2. theorem OAI.DiscreteFree.MetricWedge.discrete line 34
  3. theorem OAI.DiscreteFree.MetricWedge.retain_idempotent line 52
  4. def OAI.DiscreteFree.MetricWedge.Retained line 58
  5. instance OAI.DiscreteFree.MetricWedge.(instance at line 60) line 60
  6. def OAI.DiscreteFree.MetricWedge.retainedBase line 63
  7. def OAI.DiscreteFree.MetricWedge.collapse line 65
  8. def OAI.DiscreteFree.MetricWedge.embed line 68
  9. theorem OAI.DiscreteFree.MetricWedge.collapse_base line 71
  10. theorem OAI.DiscreteFree.MetricWedge.embed_base line 75
  11. theorem OAI.DiscreteFree.MetricWedge.embed_collapse line 79
  12. theorem OAI.DiscreteFree.MetricWedge.embed_isometry line 82
  13. theorem OAI.DiscreteFree.MetricWedge.collapse_lipschitz line 87
  14. theorem OAI.DiscreteFree.MetricWedge.retained_separated line 92
  15. theorem OAI.DiscreteFree.MetricWedge.retained_radius line 97