OAI/Analysis/LipschitzFree/StatePaths.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Counting finite-state paths with bounded transitions

  1. def OAI.DiscreteFree.StatePaths.Based line 20
  2. instance OAI.DiscreteFree.StatePaths.(instance at line 24) line 24
  3. def OAI.DiscreteFree.StatePaths.vertex line 31
  4. theorem OAI.DiscreteFree.StatePaths.at_zero line 35
  5. theorem OAI.DiscreteFree.StatePaths.at_succ line 38
  6. theorem OAI.DiscreteFree.StatePaths.at_transition line 41
  7. def OAI.DiscreteFree.StatePaths.ofSequence line 52
  8. theorem OAI.DiscreteFree.StatePaths.at_ofSequence line 57
  9. theorem OAI.DiscreteFree.StatePaths.card_based_le line 71
  10. def OAI.DiscreteFree.StatePaths.Path line 88
  11. instance OAI.DiscreteFree.StatePaths.(instance at line 90) line 90
  12. def OAI.DiscreteFree.StatePaths.Path.vertex line 92
  13. theorem OAI.DiscreteFree.StatePaths.card_path_le line 94