Commit 2025-08-30 23:52 d34daead
View on Github →feat(SimpleGraph/Bipartite): weaken finiteness assumptions (#29131) Weaken the global assumption that the vertex set was finite to the local assumption that the set of neighbors is finite for these lemmas.