Theorem SimpleGraph.neighborSet_subset_support

Modification history

2025-02-13 21:25
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat(Combinatorics/SimpleGraph): prove finite results for induced subgraphs of `G.support` (#20825) …
Added SimpleGraph.neighborSet_subset_supportView on Github →