OAI/Analysis/LipschitzFree/GraphColoring.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Rare matched walks and the fixed all-colorings graph sequence

  1. theorem OAI.DiscreteFree.GraphProducer.rare_matched_bound line 20
  2. def OAI.DiscreteFree.GraphProducer.Vertex line 85
  3. instance OAI.DiscreteFree.GraphProducer.(instance at line 87) line 87
  4. instance OAI.DiscreteFree.GraphProducer.(instance at line 90) line 90
  5. def OAI.DiscreteFree.GraphProducer.sequenceGraph line 92
  6. def OAI.DiscreteFree.GraphProducer.sequenceColor line 100
  7. def OAI.DiscreteFree.GraphProducer.intoSequence line 102
  8. theorem OAI.DiscreteFree.GraphProducer.sequence_move line 105
  9. theorem OAI.DiscreteFree.GraphProducer.sequence_walk line 110
  10. theorem OAI.DiscreteFree.GraphProducer.sequence_matched line 121
  11. theorem OAI.DiscreteFree.GraphProducer.sequence_good line 131