OAI/Combinatorics/Ramsey/CycleClique/FiniteGraphs.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.chosenChain line 22
  2. theorem OAI.CycleClique.chosenChain_sublist line 25
  3. theorem OAI.CycleClique.ClosedChain.four line 33
  4. theorem OAI.CycleClique.ClosedChain.chosen_rep line 48
  5. theorem OAI.CycleClique.ClosedChain.interior_count line 62
  6. theorem OAI.CycleClique.ClosedChain.chosen_count line 74
  7. theorem OAI.CycleClique.PathSystem.orient_rep_chain line 99
  8. theorem OAI.CycleClique.PathSystem.chosen_rep line 106
  9. theorem OAI.CycleClique.PathSystem.chosen_pair line 112
  10. def OAI.CycleClique.PathSystem.chosen line 141
  11. theorem OAI.CycleClique.PathSystem.chosen_sublist line 144
  12. theorem OAI.CycleClique.PathSystem.chosen_count line 153
  13. theorem OAI.CycleClique.OutsidePath.symm line 192
  14. theorem OAI.CycleClique.LargeSystem.exclude_two_full line 204
  15. theorem OAI.CycleClique.LargeSystem.contradiction line 249
  16. structure OAI.CycleClique.FiniteHyp line 268
  17. theorem OAI.CycleClique.FiniteHyp.degree line 282
  18. theorem OAI.CycleClique.FiniteHyp.ball_zero_size line 285
  19. theorem OAI.CycleClique.FiniteHyp.ball_zero_pair line 304
  20. theorem OAI.CycleClique.FiniteHyp.ball_step_size line 321
  21. theorem OAI.CycleClique.FiniteHyp.ball_pair line 332
  22. theorem OAI.CycleClique.FiniteHyp.ball_triple line 340
  23. theorem OAI.CycleClique.FiniteHyp.ball_stagnation line 346
  24. def OAI.CycleClique.labelAdj line 389
  25. instance OAI.CycleClique.(instance at line 390) line 390
  26. def OAI.CycleClique.LabelValid line 395
  27. instance OAI.CycleClique.(instance at line 402) line 402
  28. structure OAI.CycleClique.LabelState line 407
  29. def OAI.CycleClique.LabelState.vertices line 420
  30. theorem OAI.CycleClique.LabelState.mem_vertices line 422
  31. theorem OAI.CycleClique.LabelState.card_vertices line 424
  32. theorem OAI.CycleClique.LabelState.card_clique line 428
  33. theorem OAI.CycleClique.LabelState.mem_clique line 431
  34. def OAI.CycleClique.LabelState.system line 442
  35. theorem OAI.CycleClique.LabelState.system_chains line 488
  36. theorem OAI.CycleClique.LabelState.system_amount line 491
  37. theorem OAI.CycleClique.LabelState.system_edges line 495
  38. theorem OAI.CycleClique.LabelState.system_incident line 499