Theorem SimpleGraph.map_neighborFinset_induce

Modification history

2025-05-06 05:41

Mathlib/Combinatorics/SimpleGraph/Finite.lean

fix(SimpleGraph): drop some `DecidableEq` assumptions (#24623)

Modified SimpleGraph.map_neighborFinset_induce View on Github →

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 View on Github →