Theorem SimpleGraph.bot_preconnected
Modification history
2025-09-23 06:31
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
feat: the complete graph is connected iff nonempty (#29901) …
Deleted SimpleGraph.bot_preconnectedView on Github →