Commit 2025-12-01 21:12 02df0941

View on Github →

feat(SimpleGraph): deleteEdges distributes over sup (#31692) ... and other lemmas From ProofBench

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

added theorem SimpleGraph.deleteEdges_fromEdgeSet

added theorem SimpleGraph.deleteEdges_sup

modified theorem SimpleGraph.edgeFinset_deleteEdges