OAI/Analysis/LipschitzFree/MetricBlock.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Metric blocks obtained by adjoining finite label anchors

  1. def OAI.DiscreteFree.MetricBlock.originalLabel line 19
  2. def OAI.DiscreteFree.MetricBlock.Anchor line 22
  3. instance OAI.DiscreteFree.MetricBlock.(instance at line 24) line 24
  4. def OAI.DiscreteFree.MetricBlock.Point line 26
  5. instance OAI.DiscreteFree.MetricBlock.(instance at line 28) line 28
  6. def OAI.DiscreteFree.MetricBlock.ofVertex line 30
  7. def OAI.DiscreteFree.MetricBlock.ofAnchor line 32
  8. def OAI.DiscreteFree.MetricBlock.anchorOf line 34
  9. def OAI.DiscreteFree.MetricBlock.label line 36
  10. def OAI.DiscreteFree.MetricBlock.Adj line 40
  11. theorem OAI.DiscreteFree.MetricBlock.adj_symm line 42
  12. theorem OAI.DiscreteFree.MetricBlock.adj_comm line 46
  13. def OAI.DiscreteFree.MetricBlock.weight line 48
  14. theorem OAI.DiscreteFree.MetricBlock.weight_self line 55
  15. theorem OAI.DiscreteFree.MetricBlock.weight_symm line 58
  16. theorem OAI.DiscreteFree.MetricBlock.weight_pos line 66
  17. theorem OAI.DiscreteFree.MetricBlock.weight_zero line 74
  18. abbrev OAI.DiscreteFree.MetricBlock.metric line 80
  19. instance OAI.DiscreteFree.MetricBlock.(instance at line 84) line 84
  20. theorem OAI.DiscreteFree.MetricBlock.dist_eq line 88
  21. theorem OAI.DiscreteFree.MetricBlock.separated line 91
  22. theorem OAI.DiscreteFree.MetricBlock.weight_bound line 95
  23. theorem OAI.DiscreteFree.MetricBlock.diameter_bound line 105
  24. theorem OAI.DiscreteFree.MetricBlock.source_edge line 109
  25. theorem OAI.DiscreteFree.MetricBlock.attachment line 122
  26. theorem OAI.DiscreteFree.MetricBlock.originalLabel_step line 129
  27. theorem OAI.DiscreteFree.MetricBlock.label_weight line 141
  28. theorem OAI.DiscreteFree.MetricBlock.label_lipschitz line 170