Definitions.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact cycle–clique Ramsey statements

The red edges are the edges of G; a blue clique is an independent set in G. The cycle is a non-induced copy on exactly m distinct vertices. For the main theorem all cycle lengths are at least three.

def OAI.CycleClique.Construction.cycleNext line 19
Source documentation
Cyclic successor, defined also for the empty index type.
```
def cycleNext {m : ℕ} (i : Fin m) : Fin m :=
…
```
def OAI.CycleClique.Construction.HasCycle line 23
Source documentation
An injectively labelled cycle, including its closing edge.
```
def HasCycle (G : SimpleGraph V) (m : ℕ) : Prop :=
…
```
def OAI.CycleClique.Construction.HasIndependent line 27
Source documentation
An independent set of exactly n vertices.
```
def HasIndependent (G : SimpleGraph V) (n : ℕ) : Prop :=
…
```
def OAI.CycleClique.Construction.RamseyProperty line 31
Source documentation
The red-cycle/blue-clique property at order N.
```
def RamseyProperty (m n N : ℕ) : Prop :=
…
```
def OAI.CycleClique.Construction.IsRamseyNumber line 35
Source documentation
Specifying the least forcing order avoids an existence convention for sInf.
```
def IsRamseyNumber (m n N : ℕ) : Prop :=
…
```
theorem OAI.CycleClique.Construction.HasCycle.map line 38
theorem OAI.CycleClique.Construction.HasIndependent.map line 44
theorem OAI.CycleClique.Construction.HasIndependent.card_le line 50
theorem OAI.CycleClique.Construction.HasCycle.card_le line 55