Basic facts about diameter

Stream: graph theory

[Bernardo Anibal Subercaseaux Roa]

Hi! I wrote some proofs of basic facts about the diam/ediam that I needed for a project, and I'm wondering if it would be worth doing a PR for Mathlib (and if so, I'd appreciate any feedback on how to improve it). The concrete basic facts are here

[Bernardo Anibal Subercaseaux Roa]

For context, I needed some of these for a proof of the fact that on vertex-transitive graphs (finite and connected) the diameter is less than twice the average distance between vertices. I presume that that part is too specific for Mathlib, but maybe I'm wrong

[Rida Hamadani]

Hi @Bernardo Anibal Subercaseaux Roa, some of the lemmas in the file you link already exists here, sometimes you use the contrapose of these lemmas, I think adding that is useful to help with exact? library search.

Instead of using 1 < |α|, we usually use Nontrivial α. Fintype α is not necessary in any of the lemmas, and the reason you had to use it is so you can use Fintype.card α, but if you use Nontrivial α instead you won't need to assume finiteness.

Also, there are some naming mistakes such as how diam_eq_zero_of_not_connected should be not_connected_of_diam_eq_zero instead.

[Rida Hamadani]

other than the diameter lemmas, I believe VertexTransitive belongs to mathlib, including an API that possibly contains the result you mentioned (I do not think it is too specific, and seems useful for some of my work).

[Bernardo Anibal Subercaseaux Roa]

Thanks for your suggestions! I changed to Nontrivial \alpha and indeed could get rid of most Fintype, also fixed the incorrect naming. (File here) the one in not_connected_of_diam_zero shouldn't be possible to eliminate, since an infinite connected graph can have infinite ediam and thus diam = 0.

[Bernardo Anibal Subercaseaux Roa]

I didn't get which one of the lemmas in my file already are in mathlib though

[Rida Hamadani]

Bernardo Anibal Subercaseaux Roa said:

I didn't get which one of the lemmas in my file already are in mathlib though

For example, pos_diam_iff_ne_top_and_nt is docs#SimpleGraph.diam_eq_zero and preconnected_of_ediam_ne_top is mt G.ediam_eq_top_of_not_preconnected.
I still think having those variants in mathlib is useful for library search tools, but they should be proven using the already existing statements (which would be a 1 line proof).

[Rida Hamadani]

Good point about not_connected_of_diam_zero, I think it is nicer to add it as an iff statement (using SimpleGraph.diam_eq_zero_of_not_connected)

[Bernardo Anibal Subercaseaux Roa]

you're right! thanks :) I addressed these points!

[Rida Hamadani]

Great! I still have some style comments but these can be discussed more easily in the medium of PR reviews, please notify me (or request my review) when you open one.