OAI/Combinatorics/Ramsey/CycleClique/Construction/DenseLayers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A dense distance layer

The parity-union expansion and the numerical growth contradiction force a dense layer among the first s layers. The even case is weakly dense; the odd case is strictly dense, as in Proposition clq:layer-interface.

  1. theorem OAI.CycleClique.Construction.exists_dense_distance_layer_even line 14
  2. theorem OAI.CycleClique.Construction.exists_dense_distance_layer_odd line 59