Commit 2026-06-30 22:28 8e2ecc99

View on Github →

feat(SimpleGraph): add universal vertex predicate (#38589) Add the predicate G.IsUniversal v to indicate that v is a universal vertex, i.e. connected to all other vertices in G. This matches the recently added G.IsIsolated v predicate for isolated vertices.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.IsIsolated.not_isUniversal

added theorem SimpleGraph.IsUniversal.not_isIsolated

added theorem SimpleGraph.IsUniversal.of_subsingleton

added def SimpleGraph.IsUniversal

added theorem SimpleGraph.eq_top_iff_forall_isUniversal

added theorem SimpleGraph.insert_neighborSet_eq_univ

deleted theorem SimpleGraph.isIsolated_bot

added theorem SimpleGraph.isIsolated_compl_iff_isUniversal

added theorem SimpleGraph.isUniversal_compl_iff_isIsolated

added theorem SimpleGraph.neighborSet_eq_compl_singleton

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.Connected.of_isUniversal

added theorem SimpleGraph.Reachable.of_isUniversal

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.degree_eq_card_sub_one

added theorem SimpleGraph.degree_lt_card_sub_one

added theorem SimpleGraph.insert_neighborFinset_eq_univ

added theorem SimpleGraph.neighborFinset_eq_erase_univ

Modified Mathlib/Combinatorics/SimpleGraph/Star.lean

modified theorem SimpleGraph.connected_starGraph

added theorem SimpleGraph.isUniversal_starGraph_self

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Modified Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

modified def SimpleGraph.universalVerts