feat(Combinatorics/SimpleGraph): Define diameter of simple graphs and provide basic lemmas related to it

[Rida-Hamadani]

trafficstars

This defines the diameter of a simple graph, and provides a basic API for it.

Co-authored-by: Matt Diamond [email protected]

---

• [ ] depends on: #11945

[github-actions[bot]]

PR summary de05e50d60

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Diam	593

---

Declarations diff

+ diam + diam_anti_of_ediam_ne_top + diam_bot + diam_def + diam_eq_one + diam_eq_zero + diam_eq_zero_of_ediam_eq_top + diam_eq_zero_of_not_connected + diam_top + dist_le_diam + ediam + ediam_anti + ediam_bot + ediam_def + ediam_eq_one + ediam_eq_top + ediam_eq_top_of_not_connected + ediam_eq_top_of_not_preconnected + ediam_eq_zero_iff_subsingleton + ediam_eq_zero_of_subsingleton + ediam_le_iff + ediam_le_of_edist_le + ediam_ne_top_of_diam_ne_zero + ediam_ne_zero + ediam_ne_zero_iff_nontrivial + ediam_top + edist_le_ediam + exists_dist_eq_diam + exists_edist_eq_ediam_of_finite + exists_edist_eq_ediam_of_ne_top + exists_eq_ciInf_of_finite + exists_eq_ciSup_of_finite + exists_eq_iSup_of_lt_top + exists_eq_iSup₂_of_lt_top + nontrivial_of_diam_ne_zero + nontrivial_of_ediam_ne_zero + subsingleton_of_ediam_eq_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11945~~
• ~~leanprover-community/mathlib4#15675~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kmill]

Thanks!

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style