Commit 2023-07-21 12:37 e11c53bc
View on Github →feat: infinite (preconnected, locally finite) graphs have nonempty ends (#5916) Port/review of [mathlib#18410](https://github.com/leanprover-community/mathlib/pull/18410) directly to Mathlib4.
feat: infinite (preconnected, locally finite) graphs have nonempty ends (#5916) Port/review of [mathlib#18410](https://github.com/leanprover-community/mathlib/pull/18410) directly to Mathlib4.