Theorem SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset

Modification history

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