Commit 2025-02-13 21:25 1a4b99a6

View on Github →

feat(Combinatorics/SimpleGraph): prove finite results for induced subgraphs of G.support (#20825) Prove the edges and degrees in the induced subgraphs of G.support are equal to the edges and degrees in the original simple graph.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.neighborSet_subset_support

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.card_edgeFinset_induce_of_support_subset

added theorem SimpleGraph.card_edgeFinset_induce_support

added theorem SimpleGraph.degree_induce_of_neighborSet_subset

added theorem SimpleGraph.degree_induce_of_support_subset

added theorem SimpleGraph.degree_induce_support

added theorem SimpleGraph.edgeFinset_subset_sym2_of_support_subset

added theorem SimpleGraph.map_edgeFinset_induce

added theorem SimpleGraph.map_edgeFinset_induce_of_support_subset

added theorem SimpleGraph.map_neighborFinset_induce

added theorem SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset