OAI/Combinatorics/Ramsey/CycleClique/ExteriorPaths.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.exteriorEdges_le line 10
  2. def OAI.CycleClique.OutsidePath line 14
  3. def OAI.CycleClique.outsideBall line 20
  4. theorem OAI.CycleClique.outsideBall_subset_compl line 24
  5. theorem OAI.CycleClique.outsideBall_subset_succ line 28
  6. theorem OAI.CycleClique.outsideBall_mono line 32
  7. theorem OAI.CycleClique.closedNeighborhood_ball_subset line 36
  8. theorem OAI.CycleClique.outsideBall_walk line 46
  9. theorem OAI.CycleClique.outsidePath_of_exterior_walk line 78
  10. theorem OAI.CycleClique.outsidePath_of_balls_meet line 101
  11. theorem OAI.CycleClique.outsidePath_of_balls_adj line 117
  12. theorem OAI.CycleClique.outside_balls_separated line 138
  13. theorem OAI.CycleClique.outsidePath_of_ball_adj line 153
  14. theorem OAI.CycleClique.outside_ball_misses line 169