Commit 2025-09-23 06:31 a9a54f80

View on Github →

feat: the complete graph is connected iff nonempty (#29901) Also fix the names of a bunch of lemmas. From the ProofBench workshop

Estimated changes

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

deleted theorem SimpleGraph.bot_not_connected

deleted theorem SimpleGraph.bot_not_preconnected

deleted theorem SimpleGraph.bot_preconnected

deleted theorem SimpleGraph.bot_preconnected_iff_subsingleton

added theorem SimpleGraph.connected_bot_iff

added theorem SimpleGraph.connected_top

added theorem SimpleGraph.connected_top_iff

added theorem SimpleGraph.not_connected_bot

added theorem SimpleGraph.not_preconnected_bot

added theorem SimpleGraph.preconnected_bot

added theorem SimpleGraph.preconnected_bot_iff_subsingleton

added theorem SimpleGraph.preconnected_top

added theorem SimpleGraph.reachable_top

deleted theorem SimpleGraph.top_connected

deleted theorem SimpleGraph.top_preconnected

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.comap_bot

added theorem SimpleGraph.comap_top

added theorem SimpleGraph.induce_top