OAI/Analysis/LipschitzFree/PortGraphs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Port graphs, reduced walks, and capped-distance labels

  1. structure OAI.DiscreteFree.PortGraph line 17
  2. def OAI.DiscreteFree.PortGraph.incidenceReverse line 26
  3. theorem OAI.DiscreteFree.PortGraph.incidenceReverse_apply line 31
  4. def OAI.DiscreteFree.PortGraph.walk line 34
  5. theorem OAI.DiscreteFree.PortGraph.walk_nil line 38
  6. theorem OAI.DiscreteFree.PortGraph.walk_cons line 39
  7. theorem OAI.DiscreteFree.PortGraph.walk_append line 42
  8. def OAI.DiscreteFree.PortGraph.Reduced line 48
  9. def OAI.DiscreteFree.PortGraph.Near line 50
  10. theorem OAI.DiscreteFree.PortGraph.near_self line 52
  11. theorem OAI.DiscreteFree.PortGraph.near_mono line 54
  12. theorem OAI.DiscreteFree.PortGraph.near_step line 59
  13. def OAI.DiscreteFree.PortGraph.label line 64
  14. theorem OAI.DiscreteFree.PortGraph.label_le line 68
  15. theorem OAI.DiscreteFree.PortGraph.label_le_of_walk line 71
  16. theorem OAI.DiscreteFree.PortGraph.label_own_color line 75
  17. theorem OAI.DiscreteFree.PortGraph.label_witness line 79
  18. theorem OAI.DiscreteFree.PortGraph.label_step_le line 86
  19. theorem OAI.DiscreteFree.PortGraph.label_step_abs line 95
  20. def OAI.DiscreteFree.BoundedWords line 108
  21. instance OAI.DiscreteFree.(instance at line 110) line 110
  22. def OAI.DiscreteFree.BoundedWords.zeroEquiv line 116
  23. def OAI.DiscreteFree.BoundedWords.succEquiv line 122
  24. theorem OAI.DiscreteFree.BoundedWords.card_zero line 132
  25. theorem OAI.DiscreteFree.BoundedWords.card_succ line 135
  26. theorem OAI.DiscreteFree.BoundedWords.card_lt_pow line 140
  27. theorem OAI.DiscreteFree.PortGraph.near_finite line 154
  28. theorem OAI.DiscreteFree.PortGraph.near_card_le line 166
  29. theorem OAI.DiscreteFree.PortGraph.label_support_le line 175