G.chromaticNumber ≤ n → G.Colorable n

Stream: graph theory

[Iván Renison]

Hello, I'm trying to prove this:

theorem chromaticNumber_le_then_colorable {G : SimpleGraph α} {n : ℕ} (hc : G.chromaticNumber ≤ n) :
    G.Colorable n := by sorry

But I'm not being able to
There is a theorem that says (hc : G.Colorable m) → G.Colorable G.chromaticNumber but I'm not being able to us it because what I have is different
How could I do?

[Yaël Dillies]

docs#SimpleGraph.Colorable.mono

[Iván Renison]

I'm not able to get that G is colorable with some number, so I don't no how to get the hc parameter for Colorable.mono

[Mauricio Collares]

Do you have any other hypotheses which imply the graph can be coloured with finitely many colours?

[Yaël Dillies]

If not, then the theorem is wrong as it could be that G.chromaticNumber = 0.

[Iván Renison]

I can add that α is not empty

[Iván Renison]

So with that I think that G.chromaticNumber > 0

[Iván Renison]

I can also add that α is finite, but the I think that the theorem should be valid with α infinity, it's correct that?

[Mauricio Collares]

If G is an infinite complete graph and n is any positive integer, then the theorem is false

[Kyle Miller]

If G is not colorable with finitely many colors, then you'd have G.chromaticNumber = 0 but not G.Colorable n.

[Kyle Miller]

I've been meaning to get around to upgrading this API by making chromaticNumber be a docs#ENat

[Kyle Miller]

Another solution would be to have a G.chromaticNumberLE n style of predicate, but that's more limited than an ENat I think

[Iván Renison]

Okey, I didn't had in mind that "If G isn't colorable with finitely many colors, this will be 0."

[Iván Renison]

I will add that α is finite

[Iván Renison]

Thank you vary much

[Kyle Miller]

One way the library works right now is to include the assumption that the chromatic number is positive, or to include the assumption that there exists some n' such that G.colorable n'

[Kyle Miller]

This can be useful for you: docs#SimpleGraph.colorable_of_chromaticNumber_pos

[Iván Renison]

Yes, it seems good idea

[Iván Renison]

Thanks

[Kyle Miller]

If anyone wants to help clean this up (or maybe finish it -- I haven't checked if mathlib builds completely), #8883 refactors chromaticNumber to be ENat-valued.

[Peter Nelson]

Chromatic number is in the same boat as a few other combinatorial parameters, where ENat is the ‘right thing’ for its definition, but 95% of the work done on chromatic number is for finite graphs, and the extended type is bound to be more fiddly to deal with.

I don’t know what the best solution is to this, and it applies more generally to a lot of definitions in combinatorics of the form ‘minimum k such that [something which clearly holds for some natural number k when everything is finite]’.

[Johan Commelin]

Does the fincard and natDegree approach work? Where there are two versions of the concept, one Nat-value, and one valued in "almost Nat"?