ChromaticBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A chromatic lower bound for finite graphs with independence number at most two.

theorem OAI.HadwigerMatching.card_le_twice_of_coloring line 17
Source documentation
Every color fiber is an independent vertex set, so a coloring by k colors can cover at most 2*k vertices under the stated independence bound.
```
theorem card_le_twice_of_coloring {k : ℕ} (C : G.Coloring (Fin k))
    (hα : ∀ S : Finset V, G.IsIndepSet (S : Set V) → S.card ≤ 2) :
    Fintype.card V ≤ 2 * k := by
…
```
theorem OAI.HadwigerMatching.card_le_twice_chromaticNumber line 38
Source documentation
A finite graph has finite chromatic number; an optimal coloring then proves the lower bound, including the empty vertex type.
```
theorem card_le_twice_chromaticNumber
    (hα : ∀ S : Finset V, G.IsIndepSet (S : Set V) → S.card ≤ 2) :
    Fintype.card V ≤ 2 * G.chromaticNumber.toNat := by
…
```
theorem OAI.HadwigerMatching.card_le_twice_chromaticNumber_of_indepNum line 51
Source documentation
A graph with independence number at most two needs at least half as many colors as vertices.
```
theorem card_le_twice_chromaticNumber_of_indepNum (hα : G.indepNum ≤ 2) :
    Fintype.card V ≤ 2 * G.chromaticNumber.toNat := by
…
```