Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor: single-edge graph #9736

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - refactor: single-edge graph #9736

wants to merge 8 commits into from

Conversation

Parcly-Taxel
Copy link
Collaborator

@Parcly-Taxel Parcly-Taxel commented Jan 14, 2024 •
edited
Loading

From #9267 (comment):

I would prefer we use lattice operations for adding edges. The idea is to make constructor SimpleGraph.edge (v w : V) : SimpleGraph V that creates a graph with a single edge between v and w if they're not equal (and no edge if they are), and then G.addEdge v w would instead be G ⊔ edge v w. This is more versatile, though perhaps lemmas such as addEdge_of_adj are a bit more brittle to apply.

Open in Gitpod

@Parcly-Taxel Parcly-Taxel added awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Jan 14, 2024
@Parcly-Taxel Parcly-Taxel mentioned this pull request Jan 14, 2024
Closed
lambda-fairy
lambda-fairy reviewed Mar 18, 2024
View reviewed changes
Copy link
Collaborator

@lambda-fairy lambda-fairy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is pretty cool. I assume we can delete an edge with G \ edge v w too?

Mathlib/Combinatorics/SimpleGraph/Operations.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/SimpleGraph/Operations.lean Outdated Show resolved Hide resolved
kmill
kmill approved these changes Mar 18, 2024
View reviewed changes
Copy link
Contributor

@kmill kmill left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for following up on this idea. Once you get that spacing fixed, and decide how to address edge_self_eq_bot, we'll merge.

@Parcly-Taxel
Copy link
Collaborator Author

@kmill done.

@Parcly-Taxel Parcly-Taxel requested a review from kmill March 19, 2024 19:59
@kmill
Copy link
Contributor

kmill commented Mar 19, 2024

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2024
@Parcly-Taxel
refactor: single-edge graph (#9736)
7898bcf 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 19, 2024

Build failed (retrying...):

  • Build

mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2024
@Parcly-Taxel
refactor: single-edge graph (#9736)
ee8a551 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 19, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Mar 19, 2024
@Parcly-Taxel
refactor: single-edge graph (#9736)
69fd837 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: single-edge graph [Merged by Bors] - refactor: single-edge graph Mar 19, 2024
@mathlib-bors mathlib-bors bot closed this Mar 19, 2024
@mathlib-bors mathlib-bors bot deleted the trabant branch March 19, 2024 23:30
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@Parcly-Taxel @dagurtomas
refactor: single-edge graph (#9736)
22a15c6 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
utensil pushed a commit that referenced this pull request Mar 26, 2024
@Parcly-Taxel @utensil
refactor: single-edge graph (#9736)
aecc209 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@Parcly-Taxel @Louddy
refactor: single-edge graph (#9736)
edd5122 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@Parcly-Taxel @atarnoam
refactor: single-edge graph (#9736)
e8681d5 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@Parcly-Taxel @uniwuni
refactor: single-edge graph (#9736)
4d4d8a5 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@Parcly-Taxel @callesonne
refactor: single-edge graph (#9736)
7b5a508 
From #9267 (comment):
> I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lambda-fairy lambda-fairy lambda-fairy left review comments

@kmill kmill Awaiting requested review from kmill

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Parcly-Taxel @kmill @lambda-fairy