OAI/Combinatorics/IndependentSets/Reduction/WalkLength.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.walkLength line 8
  2. def OAI.LargeIndependentSets.pathDistance line 12
  3. lemma OAI.LargeIndependentSets.pathDistance_le_link line 15
  4. lemma OAI.LargeIndependentSets.walkLength_append line 19
  5. lemma OAI.LargeIndependentSets.pathDistance_self line 26
  6. lemma OAI.LargeIndependentSets.pathDistance_triangle line 30
  7. lemma OAI.LargeIndependentSets.walkLength_map line 41
  8. lemma OAI.LargeIndependentSets.pathDistance_invariant line 48
  9. lemma OAI.LargeIndependentSets.nonexpanding_path line 58
  10. lemma OAI.LargeIndependentSets.walkLength_reverse line 69
  11. lemma OAI.LargeIndependentSets.pathDistance_symm line 78
  12. abbrev OAI.LargeIndependentSets.linkPseudoEMetric line 87
  13. def OAI.LargeIndependentSets.circleRep line 93
  14. lemma OAI.LargeIndependentSets.circleRep_nonneg line 96
  15. lemma OAI.LargeIndependentSets.circleRep_lt_one line 99
  16. lemma OAI.LargeIndependentSets.circleRep_coe line 102
  17. def OAI.LargeIndependentSets.circleColor line 105
  18. lemma OAI.LargeIndependentSets.circleColor_bounds line 108
  19. lemma OAI.LargeIndependentSets.circle_dist_le_reps line 120
  20. lemma OAI.LargeIndependentSets.circle_same_color_close line 130
  21. lemma OAI.LargeIndependentSets.circle_antipode_distance line 139
  22. theorem OAI.LargeIndependentSets.phase_completeness line 144
  23. structure OAI.LargeIndependentSets.ProjectionSystem line 166
  24. abbrev OAI.LargeIndependentSets.GridLocation line 169
  25. def OAI.LargeIndependentSets.ProjectionSystem.Consistent line 172
  26. inductive OAI.LargeIndependentSets.ProjectionSystem.ForwardZero line 176
  27. def OAI.LargeIndependentSets.ProjectionSystem.ZeroLink line 181
  28. def OAI.LargeIndependentSets.copyLength line 185
  29. lemma OAI.LargeIndependentSets.copyLength_same line 192
  30. def OAI.LargeIndependentSets.ProjectionSystem.linkLength line 198
  31. def OAI.LargeIndependentSets.gridPhase line 204
  32. lemma OAI.LargeIndependentSets.forwardZero_phase line 208
  33. lemma OAI.LargeIndependentSets.zeroLink_phase line 215
  34. lemma OAI.LargeIndependentSets.gridPhase_nonexpanding line 223
  35. def OAI.LargeIndependentSets.gridAntipode line 239
  36. lemma OAI.LargeIndependentSets.grid_half_real line 243
  37. lemma OAI.LargeIndependentSets.gridPhase_antipode line 252
  38. lemma OAI.LargeIndependentSets.gridAntipode_involutive line 257
  39. theorem OAI.LargeIndependentSets.projection_grid_completeness line 268
  40. lemma OAI.LargeIndependentSets.copyLength_self line 280
  41. lemma OAI.LargeIndependentSets.copyLength_symm line 285
  42. lemma OAI.LargeIndependentSets.zeroLink_symm line 295
  43. lemma OAI.LargeIndependentSets.linkLength_self line 299
  44. lemma OAI.LargeIndependentSets.linkLength_symm line 304
  45. lemma OAI.LargeIndependentSets.forwardZero_antipode line 310
  46. lemma OAI.LargeIndependentSets.zeroLink_antipode line 317
  47. lemma OAI.LargeIndependentSets.zeroLink_antipode_iff line 324
  48. lemma OAI.LargeIndependentSets.copyLength_antipode line 333
  49. lemma OAI.LargeIndependentSets.linkLength_antipode line 344
  50. lemma OAI.LargeIndependentSets.twisted_pathDistance_symm line 351
  51. def OAI.LargeIndependentSets.gridGraph line 363
  52. theorem OAI.LargeIndependentSets.gridGraph_three_coloring line 375