OAI/Analysis/LipschitzFree/MetricClosure.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Integer shortest-path metrics and Lipschitz descent

  1. def OAI.DiscreteFree.NatMetricClosure.cost line 19
  2. theorem OAI.DiscreteFree.NatMetricClosure.cost_nil line 23
  3. theorem OAI.DiscreteFree.NatMetricClosure.cost_cons line 24
  4. theorem OAI.DiscreteFree.NatMetricClosure.cost_append line 27
  5. theorem OAI.DiscreteFree.NatMetricClosure.cost_reverse line 33
  6. def OAI.DiscreteFree.NatMetricClosure.distance line 41
  7. theorem OAI.DiscreteFree.NatMetricClosure.distance_le_cost line 44
  8. theorem OAI.DiscreteFree.NatMetricClosure.exists_shortest line 47
  9. theorem OAI.DiscreteFree.NatMetricClosure.distance_le line 50
  10. theorem OAI.DiscreteFree.NatMetricClosure.distance_self line 52
  11. theorem OAI.DiscreteFree.NatMetricClosure.distance_comm line 57
  12. theorem OAI.DiscreteFree.NatMetricClosure.distance_triangle line 67
  13. theorem OAI.DiscreteFree.NatMetricClosure.cost_zero line 75
  14. theorem OAI.DiscreteFree.NatMetricClosure.distance_zero line 83
  15. abbrev OAI.DiscreteFree.NatMetricClosure.metricSpace line 88
  16. theorem OAI.DiscreteFree.NatMetricClosure.separated line 96
  17. theorem OAI.DiscreteFree.NatMetricClosure.lipschitz_bound line 104
  18. theorem OAI.DiscreteFree.NatMetricClosure.path_relation line 118