OAI/Analysis/LipschitzFree/Wedge.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Metric wedges and their contractive component retractions

  1. def OAI.DiscreteFree.MetricWedge.Point line 18
  2. instance OAI.DiscreteFree.MetricWedge.(instance at line 20) line 20
  3. def OAI.DiscreteFree.MetricWedge.base line 23
  4. def OAI.DiscreteFree.MetricWedge.distance line 25
  5. theorem OAI.DiscreteFree.MetricWedge.distance_self line 32
  6. theorem OAI.DiscreteFree.MetricWedge.distance_comm line 35
  7. theorem OAI.DiscreteFree.MetricWedge.distance_triangle line 41
  8. theorem OAI.DiscreteFree.MetricWedge.eq_of_distance_zero line 89
  9. instance OAI.DiscreteFree.MetricWedge.(instance at line 105) line 105
  10. def OAI.DiscreteFree.MetricWedge.inclusion line 112
  11. def OAI.DiscreteFree.MetricWedge.retraction line 115
  12. theorem OAI.DiscreteFree.MetricWedge.inclusion_base line 120
  13. theorem OAI.DiscreteFree.MetricWedge.retraction_base line 125
  14. theorem OAI.DiscreteFree.MetricWedge.retraction_inclusion line 128
  15. theorem OAI.DiscreteFree.MetricWedge.retraction_other line 135
  16. theorem OAI.DiscreteFree.MetricWedge.inclusion_isometry line 139
  17. theorem OAI.DiscreteFree.MetricWedge.retraction_lipschitz line 145
  18. def OAI.DiscreteFree.MetricWedge.retain line 169
  19. theorem OAI.DiscreteFree.MetricWedge.retain_base line 174
  20. theorem OAI.DiscreteFree.MetricWedge.retain_inclusion line 177
  21. theorem OAI.DiscreteFree.MetricWedge.retain_lipschitz line 181