Theorem name

Stream: graph theory

[Iván Renison]

Hello! I want to add this theorem to mathlib:

theorem name {α} {G : SimpleGraph α} {u : α} (p : G.Walk u u)
    (hOdd : Odd p.length) : 2 < G.chromaticNumber

And I was thinking the name Walk.two_le_chromaticNumber_of_odd_self but I'm not sure, especially for the part of G.Walk u u. What name do you suggest?

[Shreyas Srinivas]

chromaticNumber_graph_with_odd_cycle_gt_2?

[Iván Renison]

In Connectivity.lean a cycle is defined as a G.Walk u u witch has no repeated nodes except the first and last, so using the word cycle I think that it may be confusing, because this walk is not necessarily a cycle

[Shreyas Srinivas]

Yeah but if you have a looping walk, you have a cycle in it

[Shreyas Srinivas]

at least one of these extracted cycles must have odd length

[Mauricio Collares]

Walk.two_lt_chromaticNumber_of_odd_closed?

[Iván Renison]

That look good, thanks

[Peter Nelson]

why two_lt rather than three_le?

[Iván Renison]

I don't have to much reason, you think three_le and state the theorem with 3 ≤ is better?

[Iván Renison]

Also: you can see the code in #14409

[Kyle Miller]

I think we use the word "loop" for this, so I'd suggest Walk.two_le_chromaticNumber_of_odd_loop.

(or three_le, which seems better but I'm not sure I can say why)

[Iván Renison]

Maybe it seems better because usually in math we start integers intervals with a closed (We say [a, b))

[Peter Nelson]

To possibly state the same thing another way: three_le is a stronger statement than two_lt once you cast to rationals/reals.

[Mauricio Collares]

Huh, to me a loop is more restrictive than a closed walk; in the terminology I'm used to, a loop is a closed walk of length one, i.e. a single edge connecting a vertex to itself

[Mauricio Collares]

There's probably no confusion now because most graphs in mathlib are simple, but it could be a problem in the future

[Iván Renison]

I usually call that a self loop

[Mauricio Collares]

Just to be sure, I've just checked Bollobás, Bondy-Murty, Diestel, Harary and West, and they all use "loop" for an edge connecting a vertex to itself (curiously, they differ on whether a multigraph can have loops, but that's a different matter)

[Kyle Miller]

Did those sources have the "closed walk" terminology? If so, I think I'd be happy to see a PR that systematically replaces 'loop' with 'closed' and adds an entry to the glossary in the module in Connectivity.lean

For now though, Iván should use 'loop' to be consistent. (Edit: I just sent it to bors)

[Peter Nelson]

I work in a department full of graph theorists, go to graph theory conferences and am arguably a graph theorist myself, and I’ve never heard the word ‘loop’ used in research to refer to anything that isn’t a single edge.

I hear ‘self-loop’ sometimes but would consider it redundant and quite unusual.
‘Closed walk’ is very standard to refer to a walk with beginning and end the same.

[Mauricio Collares]

BTW, I think self-loop is popular in algorithms textbooks only because they want the word loop to be reserved to the algorithmic meaning.

[Peter Nelson]

That makes sense.