Commit 2024-08-11 20:16 5bb47cdc

View on Github →

feat(Combinatorics/SimpleGraph): bot is not connected (#15675)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.bot_not_connected

added theorem SimpleGraph.bot_not_preconnected

added theorem SimpleGraph.bot_preconnected

added theorem SimpleGraph.bot_preconnected_iff_subsingleton