Monotonicity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CycleClique.Construction.RamseyProperty.mono line 7
Source documentation
Enlarging the vertex set preserves the forcing property.
```
theorem RamseyProperty.mono {m n M N : ℕ} (h : RamseyProperty m n M) (hMN : M ≤ N) :
    RamseyProperty m n N := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty
theorem OAI.CycleClique.Construction.not_ramseyProperty_mono line 17
Source documentation
A coloring avoiding the two targets restricts to every smaller order.
```
theorem not_ramseyProperty_mono {m n M N : ℕ}
    (h : ¬ RamseyProperty m n N) (hMN : M ≤ N) : ¬ RamseyProperty m n M :=
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty
theorem OAI.CycleClique.Construction.isRamseyNumber_of_upper_lower line 22
Source documentation
A forcing upper bound and a coloring one vertex below it determine the number.
```
theorem isRamseyNumber_of_upper_lower {m n N : ℕ}
    (hupper : RamseyProperty m n (N + 1)) (hlower : ¬ RamseyProperty m n N) :
    IsRamseyNumber m n (N + 1) := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty, OAI.CycleClique.Construction.IsRamseyNumber