Theorem SimpleGraph.nonempty_ends_of_infinite

Modification history

2023-07-21 12:37
Mathlib/Combinatorics/SimpleGraph/Ends/Properties.lean
feat: infinite (preconnected, locally finite) graphs have nonempty ends (#5916) …
Added SimpleGraph.nonempty_ends_of_infiniteView on Github →