Theorem SimpleGraph.card_edgeFinset_induce_of_support_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.card_edgeFinset_induce_of_support_subsetView on Github →