OAI/Combinatorics/Ramsey/CycleClique/FrameProperties.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.Frame.Q line 31
  2. def OAI.CycleClique.Frame.U line 33
  3. theorem OAI.CycleClique.Frame.memQ line 35
  4. theorem OAI.CycleClique.Frame.cardQ line 37
  5. theorem OAI.CycleClique.Frame.clique line 41
  6. theorem OAI.CycleClique.Frame.exterior line 45
  7. theorem OAI.CycleClique.Frame.neQ line 47
  8. def OAI.CycleClique.Frame.reindex line 50
  9. theorem OAI.CycleClique.Frame.reindex_Q line 54
  10. theorem OAI.CycleClique.Frame.reindex_U line 62
  11. def OAI.CycleClique.Frame.triangle line 68
  12. theorem OAI.CycleClique.Frame.triangle_Q line 76
  13. theorem OAI.CycleClique.exists_frame line 91
  14. theorem OAI.CycleClique.extClosed_sum_bound line 99
  15. theorem OAI.CycleClique.extClosed_pair_bound line 113
  16. theorem OAI.CycleClique.extClosed_expansion line 124
  17. theorem OAI.CycleClique.extClosed_indep_expansion line 146
  18. theorem OAI.CycleClique.Frame.U_degree line 156
  19. theorem OAI.CycleClique.Frame.clique_U_bound line 174
  20. theorem OAI.CycleClique.Frame.U_ball line 187
  21. theorem OAI.CycleClique.Frame.extClosed_U_ball line 190
  22. theorem OAI.CycleClique.Frame.boundary_U line 197
  23. theorem OAI.CycleClique.Frame.disjoint_U_expansion line 208
  24. theorem OAI.CycleClique.Frame.disjoint_U_closed line 219
  25. theorem OAI.CycleClique.small_four_clique line 231
  26. structure OAI.CycleClique.FourHyp line 268