OAI/Combinatorics/SharpRamsey/Bounds/Upper.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

The off-diagonal Ramsey upper bound.

  1. theorem OAI.SharpLogRamsey.Foundation.indepNum_lt_of_cliqueFree_compl line 18
  2. theorem OAI.SharpLogRamsey.Foundation.maximum_indep_dominates line 25
  3. theorem OAI.SharpLogRamsey.Foundation.card_le_mul_indepNum line 40
  4. theorem OAI.SharpLogRamsey.Foundation.cliqueFree_neighbor line 60
  5. theorem OAI.SharpLogRamsey.Foundation.cliqueFree_induce line 67
  6. theorem OAI.SharpLogRamsey.Foundation.compl_cliqueFree_induce line 74
  7. theorem OAI.SharpLogRamsey.Foundation.order_avoiding_lt_pow line 80
  8. theorem OAI.SharpLogRamsey.Foundation.ramseyProperty_pow line 108
  9. theorem OAI.SharpLogRamsey.Foundation.ramseyProperty_nonempty line 119
  10. theorem OAI.SharpLogRamsey.Foundation.ramsey_has_property line 124
  11. theorem OAI.SharpLogRamsey.Foundation.clique_map_embedding line 128
  12. theorem OAI.SharpLogRamsey.Foundation.compl_comap_embedding line 138
  13. theorem OAI.SharpLogRamsey.Foundation.property_for_finite_type line 144
  14. theorem OAI.SharpLogRamsey.Foundation.order_lt_ramsey line 155
  15. theorem OAI.SharpLogRamsey.Foundation.ramsey_le_of_property line 163
  16. theorem OAI.SharpLogRamsey.Foundation.property_mono line 166
  17. theorem OAI.SharpLogRamsey.Foundation.ramsey_le_pow line 171
  18. theorem OAI.SharpLogRamsey.Foundation.le_ramsey line 177
  19. theorem OAI.SharpLogRamsey.Foundation.ramsey_two line 183
  20. theorem OAI.SharpLogRamsey.Foundation.cliqueFree_common line 189
  21. theorem OAI.SharpLogRamsey.Foundation.exists_avoiding_pred line 198
  22. def OAI.SharpLogRamsey.TriangleFree.independentSets line 217
  23. theorem OAI.SharpLogRamsey.TriangleFree.mem_independentSets line 220
  24. theorem OAI.SharpLogRamsey.TriangleFree.independentSets_nonempty line 224
  25. def OAI.SharpLogRamsey.TriangleFree.closed line 228
  26. def OAI.SharpLogRamsey.TriangleFree.outside line 229
  27. def OAI.SharpLogRamsey.TriangleFree.available line 230
  28. def OAI.SharpLogRamsey.TriangleFree.fiber line 232
  29. def OAI.SharpLogRamsey.TriangleFree.Admissible line 235
  30. theorem OAI.SharpLogRamsey.TriangleFree.mem_closed line 238
  31. theorem OAI.SharpLogRamsey.TriangleFree.mem_outside line 240
  32. theorem OAI.SharpLogRamsey.TriangleFree.mem_available line 243
  33. theorem OAI.SharpLogRamsey.TriangleFree.center_not_available line 247
  34. theorem OAI.SharpLogRamsey.TriangleFree.admissible_outside line 250
  35. theorem OAI.SharpLogRamsey.TriangleFree.admissible_not_center line 257
  36. theorem OAI.SharpLogRamsey.TriangleFree.admissible_not_adj line 262
  37. theorem OAI.SharpLogRamsey.TriangleFree.available_disjoint line 267
  38. theorem OAI.SharpLogRamsey.TriangleFree.independent_insert_center line 273
  39. theorem OAI.SharpLogRamsey.TriangleFree.independent_extend line 285
  40. theorem OAI.SharpLogRamsey.TriangleFree.outside_insert_center line 298
  41. theorem OAI.SharpLogRamsey.TriangleFree.outside_extend line 309
  42. theorem OAI.SharpLogRamsey.TriangleFree.fiber_eq line 322
  43. theorem OAI.SharpLogRamsey.TriangleFree.extend_injective line 371
  44. theorem OAI.SharpLogRamsey.TriangleFree.center_choice_not_image line 379
  45. theorem OAI.SharpLogRamsey.TriangleFree.card_fiber line 388
  46. theorem OAI.SharpLogRamsey.TriangleFree.sum_fiber line 394
  47. theorem OAI.SharpLogRamsey.TriangleFree.twice_sum_powerset_card line 403
  48. theorem OAI.SharpLogRamsey.TriangleFree.center_neighbor_inter line 428
  49. theorem OAI.SharpLogRamsey.TriangleFree.extend_neighbor_inter line 437