Commit 2025-04-19 03:18 323f7812

View on Github →

feat(SimpleGraph): eccentricity, radius, and center (#23932) This PR defines the eccentricity of a vertex, the radius, and the center of a simple graph, and provides an API for them. They are placed in the Diam.lean file because they are closely related and have a similar API. Also this PR redefines SimpleGraph.ediam in terms of eccentricity, which shortens some of its proofs.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

added def SimpleGraph.center

added theorem SimpleGraph.center_bot

added theorem SimpleGraph.center_eq_univ_iff_radius_eq_ediam

added theorem SimpleGraph.center_eq_univ_of_subsingleton

added theorem SimpleGraph.center_nonempty

added theorem SimpleGraph.center_top

modified theorem SimpleGraph.diam_eq_zero_of_not_connected

added theorem SimpleGraph.eccent_bot

added theorem SimpleGraph.eccent_def

added theorem SimpleGraph.eccent_eq_top_of_not_connected

added theorem SimpleGraph.eccent_eq_zero_iff

added theorem SimpleGraph.eccent_eq_zero_of_subsingleton

added theorem SimpleGraph.eccent_le_ediam

added theorem SimpleGraph.eccent_ne_zero

added theorem SimpleGraph.eccent_pos_iff

added theorem SimpleGraph.eccent_top

added theorem SimpleGraph.ediam_eq_iSup_iSup_edist

modified theorem SimpleGraph.ediam_eq_top_of_not_connected

modified theorem SimpleGraph.ediam_eq_top_of_not_preconnected

modified theorem SimpleGraph.ediam_le_of_edist_le

added theorem SimpleGraph.ediam_le_two_mul_radius

added theorem SimpleGraph.edist_le_eccent

added theorem SimpleGraph.eq_top_iff_forall_eccent_eq_one

added theorem SimpleGraph.exists_eccent_eq_ediam_of_finite

added theorem SimpleGraph.exists_eccent_eq_ediam_of_ne_top

added theorem SimpleGraph.exists_eccent_eq_radius

added theorem SimpleGraph.exists_edist_eq_eccent_of_finite

added theorem SimpleGraph.exists_edist_eq_radius_of_finite

added theorem SimpleGraph.mem_center_iff

added theorem SimpleGraph.radius_bot

added theorem SimpleGraph.radius_eq_ediam_iff

added theorem SimpleGraph.radius_eq_iInf_iSup_edist

added theorem SimpleGraph.radius_eq_top_of_isEmpty

added theorem SimpleGraph.radius_eq_top_of_not_connected

added theorem SimpleGraph.radius_eq_zero_iff

added theorem SimpleGraph.radius_le_eccent

added theorem SimpleGraph.radius_le_ediam

added theorem SimpleGraph.radius_ne_top_iff

added theorem SimpleGraph.radius_ne_zero_of_nontrivial

added theorem SimpleGraph.radius_top

Modified Mathlib/Combinatorics/SimpleGraph/Girth.lean