OAI/Combinatorics/Ramsey/CycleClique/DistanceLayers.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.ncard_union_layers line 13
  2. theorem OAI.CycleClique.sum_independence_layers line 29
  3. def OAI.CycleClique.distanceLayer line 61
  4. theorem OAI.CycleClique.distanceLayer_zero line 64
  5. theorem OAI.CycleClique.distanceLayer_disjoint line 73
  6. theorem OAI.CycleClique.distanceLayer_no_edge line 80
  7. def OAI.CycleClique.parityIndices line 90
  8. def OAI.CycleClique.paritySum line 94
  9. theorem OAI.CycleClique.paritySum_zero line 96
  10. theorem OAI.CycleClique.paritySum_add_prev line 99
  11. theorem OAI.CycleClique.parity_independence_bound line 119
  12. theorem OAI.CycleClique.independence_singleton line 130
  13. theorem OAI.CycleClique.distanceLayer_one_nonempty line 138
  14. theorem OAI.CycleClique.parity_layer_union_nonempty line 154
  15. theorem OAI.CycleClique.closedNeighborhood_parity_layers line 167
  16. theorem OAI.CycleClique.distance_layer_sum line 184
  17. theorem OAI.CycleClique.exists_dense_layer_numeric line 216
  18. theorem OAI.CycleClique.exists_dense_distance_layer line 301
  19. theorem OAI.CycleClique.exists_minimal_dense_layer line 320