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.

Estimated changes