Theorem SimpleGraph.exists_adj_iff_not_isIsolated

Modification history

2026-06-14 19:00

Mathlib/Combinatorics/SimpleGraph/Basic.lean

feat(Combinatorics/SimpleGraph/Basic): more `neighborSet` and `IsIsolated` lemmas (#38747)

Added SimpleGraph.exists_adj_iff_not_isIsolated View on Github →