[Merged by Bors] - feat(Combinatorics/Graph): graph deletion operations#35879
Closed
Jun2M wants to merge 48 commits into
Closed
[Merged by Bors] - feat(Combinatorics/Graph): graph deletion operations#35879Jun2M wants to merge 48 commits into
Jun2M wants to merge 48 commits into
Conversation
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
reviewed
Apr 8, 2026
YaelDillies
added
awaiting-author
Jun2M
removed
the
awaiting-author
YaelDillies
reviewed
Apr 9, 2026
YaelDillies
added
the
awaiting-author
Jun2M
removed
the
awaiting-author
1 task
b-mehta
reviewed
Apr 10, 2026
|
|
||
| namespace Graph | ||
|
|
||
| /-- Restrict `G : Graph α β` to the edges in a set `E₀` without removing vertices -/ |
Contributor
There was a problem hiding this comment.
Would restrictEdges make more sense here, to make it clear that this isn't restricting the vertex set? (I could imagine the restriction of a graph to a vertex set also being a reasonable informal description of induce)
Collaborator
Author
There was a problem hiding this comment.
restrict is named to mirror the name already given for SimpleGraph, SimpleGraph.Subgraph.restrict. Do you think it is still worth it to break the symmetry and change the name?
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
YaelDillies
approved these changes
Apr 14, 2026
Contributor
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
It's in @Bhavik Mehta's hands now
maintainer merge?
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
mathlib-triage
Bot
added
the
maintainer-merge
mathlib-triage
Bot
added
ready-to-merge
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Apr 15, 2026
This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations: - `restrict`: the subgraph of `G` restricted to the edges in `F` without removing vertices - `deleteEdges`: the subgraph of `G` with the edges in `F` deleted - `induce`: the subgraph of `G` induced by the set `X` of vertices - `deleteVerts` : the graph obtained from `G` by deleting the set `X` of vertices These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
jessealama
pushed a commit
to jessealama/mathlib4
that referenced
this pull request
May 2, 2026
…unity#35879) This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations: - `restrict`: the subgraph of `G` restricted to the edges in `F` without removing vertices - `deleteEdges`: the subgraph of `G` with the edges in `F` deleted - `induce`: the subgraph of `G` induced by the set `X` of vertices - `deleteVerts` : the graph obtained from `G` by deleting the set `X` of vertices These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
gaetanserre
pushed a commit
to gaetanserre/mathlib4
that referenced
this pull request
May 5, 2026
…unity#35879) This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations: - `restrict`: the subgraph of `G` restricted to the edges in `F` without removing vertices - `deleteEdges`: the subgraph of `G` with the edges in `F` deleted - `induce`: the subgraph of `G` induced by the set `X` of vertices - `deleteVerts` : the graph obtained from `G` by deleting the set `X` of vertices These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
gasparattila
pushed a commit
to gasparattila/mathlib4
that referenced
this pull request
May 9, 2026
…unity#35879) This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations: - `restrict`: the subgraph of `G` restricted to the edges in `F` without removing vertices - `deleteEdges`: the subgraph of `G` with the edges in `F` deleted - `induce`: the subgraph of `G` induced by the set `X` of vertices - `deleteVerts` : the graph obtained from `G` by deleting the set `X` of vertices These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean.
It introduces the following operations:
restrict: the subgraph ofGrestricted to the edges inFwithoutremoving vertices
deleteEdges: the subgraph ofGwith the edges inFdeletedinduce: the subgraph ofGinduced by the setXof verticesdeleteVerts: the graph obtained fromGby deleting the setXof verticesThese definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity.
Co-authored-by: Peter Nelson apn.uni@gmail.com
Graph#26770