Theorem SimpleGraph.end_componentCompl_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.end_componentCompl_infiniteView on Github →