Theorem SimpleGraph.neighborSet_mono

Modification history

2026-06-14 19:00

Mathlib/Combinatorics/SimpleGraph/Basic.lean

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

Modified SimpleGraph.neighborSet_mono View on Github →

2026-04-26 22:04

Mathlib/Combinatorics/SimpleGraph/Maps.lean

feat(Combinatorics/SimpleGraph/Maps): characterize `neighborSet` and `edgeSet` across an embedding (#35628)

Added SimpleGraph.neighborSet_mono View on Github →