Commit 2025-05-06 02:45 1bef2b39

View on Github →

feat(Combinatorics/SimpleGraph): define deleteIncidenceSet (#20681) Define the operation G.deleteIncidenceSet x deleting the incidence set of the vertex x from the edge set of the simple graph G and prove theorems in the finite case.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

added theorem SimpleGraph.card_edgeFinset_deleteIncidenceSet

added theorem SimpleGraph.card_edgeFinset_induce_compl_singleton

added theorem SimpleGraph.card_support_deleteIncidenceSet

added def SimpleGraph.deleteIncidenceSet

added theorem SimpleGraph.deleteIncidenceSet_adj

added theorem SimpleGraph.deleteIncidenceSet_le

added theorem SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter

added theorem SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff

added theorem SimpleGraph.edgeSet_deleteIncidenceSet

added theorem SimpleGraph.edgeSet_fromEdgeSet_incidenceSet

added theorem SimpleGraph.induce_deleteIncidenceSet_of_not_mem

added theorem SimpleGraph.support_deleteIncidenceSet_subset

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.incidenceFinset_subset