Skip to content

feat(Combinatorics/Graph): Add graph deletion operations#35879

Open
Jun2M wants to merge 40 commits intoleanprover-community:masterfrom
Jun2M:GraphDelete
Open

feat(Combinatorics/Graph): Add graph deletion operations#35879
Jun2M wants to merge 40 commits intoleanprover-community:masterfrom
Jun2M:GraphDelete

Conversation

@Jun2M
Copy link
Copy Markdown
Collaborator

@Jun2M Jun2M commented Feb 28, 2026 •
edited
Loading

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:

  • G ↾ F (edgeRestrict): The subgraph of G restricted to the edges in F (vertices are preserved).
  • G ＼ F (edgeDelete): The subgraph of G with the edges in F deleted.
  • G[X] (induce): The subgraph of G induced by the set of vertices X.
  • G - X (vertexDelete): The graph obtained from G by deleting the set of vertices X.

These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity.

Co-authored-by: Peter Nelson [email protected]

Open in Gitpod

Jun2M and others added 30 commits July 4, 2025 17:28
@Jun2M
Graph.Subgraph
a071be8
@Jun2M
Add docstrings
8576ce1
@Jun2M
scoping notations
fc5d553
@Jun2M
move some to finite file
e522a9a
@Jun2M
fix imports
380056e
@Jun2M
Merge branch 'master' into subgraph
80dd77b
@Jun2M
focus on relations
b1aba94
@Jun2M
Docs update
b1d595d
@Jun2M
Remove unused imports
c4a0315
@Jun2M
Merge branch 'master' into subgraph
d207dca
@Jun2M
module
d85c334
@Jun2M @YaelDillies
Remove unnecessary braket
09af04c 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M
Eq to Iff
90737a5
@Jun2M @YaelDillies
Change comments to reflect inlineing
f5f9689 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M
Apply suggested changes
7fc070d
@Jun2M @YaelDillies
Reflect copy being moved in the comment
250e8ce 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M @YaelDillies
Remove _self
b4ff78a 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M @YaelDillies
inc_inj
04640f9 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M
Compatible
212b36e
@Jun2M
nudge github action
f74dd69
@Jun2M
isInducedSubgraph_iff
8f0a6a7
@Jun2M
Merge branch 'master' into subgraph
02a2f17
@Jun2M
merge fixes
b3f3414
@Jun2M @YaelDillies
golf le_refl
70a5bb2 
Co-authored-by: Yaël Dillies <[email protected]>
@Jun2M
Comment change
48362f3
@Jun2M
Use Compatible
3a8f13a
@Jun2M
strengthen to iffs
7786c69
@Jun2M
le_iff_compatible_subset_subset
eae4edd
@Jun2M
IsSubgraph structure
ca11b5d
@Jun2M
Init
8cc1662
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 28, 2026 •
edited
Loading

PR summary cd8272a9d5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.Graph.Delete (new file) 493

Declarations diff

+ edgeDelete
+ edgeDelete_edgeDelete
+ edgeDelete_empty
+ edgeDelete_eq_edgeRestrict
+ edgeDelete_inc
+ edgeDelete_isLoopAt
+ edgeDelete_le
+ edgeDelete_mono_left
+ edgeRestrict
+ edgeRestrict_edgeRestrict
+ edgeRestrict_edgeSet_inter
+ edgeRestrict_eq_edgeDelete
+ edgeRestrict_eq_self_iff
+ edgeRestrict_inc
+ edgeRestrict_inter_edgeSet
+ edgeRestrict_isLoopAt
+ edgeRestrict_le
+ edgeRestrict_mono_left
+ edgeRestrict_mono_right
+ edgeRestrict_self
+ induce
+ induce_edgeSet
+ induce_le
+ induce_le_iff
+ induce_vertexSet_self
+ instance : HSub (Graph α β) (Set α) (Graph α β)
+ vertexDelete
+ vertexDelete_def
+ vertexDelete_edgeSet
+ vertexDelete_empty
+ vertexDelete_isLink
+ vertexDelete_le
+ vertexDelete_vertexSet

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-combinatorics Combinatorics label Feb 28, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 28, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 21, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 21, 2026

This PR/issue depends on:

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 21, 2026

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026
@Jun2M Jun2M requested a review from YaelDillies April 3, 2026 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies Awaiting requested review from YaelDillies

Assignees

No one assigned

Labels

t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Jun2M