-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(combinatorics/simple_graph): add maps and subgraphs #8223
Conversation
I think the PR would be easier to evaluate if the documentation/non-math changes were PR'd separate from the mathematical changes. The way it is now, it is difficult to find places in the diff that have the mathematical content, since there are so many lines that have been modified. |
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
…ty/mathlib into ramsey_theory
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
✌️ hmonroe can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+
|
Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed `edge_symm` to `adj_comm`. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
bors r- To be clear @hmonroe, I meant that I'm happy for this to be merged once the unresolved comments have been addressed, and at that point you are free to hit merge. |
Canceled. |
@hmonroe I'm making a couple changes |
Thanks everyone for reviewing! bors r+ |
🔒 Permission denied Existing reviewers: click here to make kmill a reviewer |
@hmonroe I forgot I've not been delegated to do the merge -- I'll leave it to you. |
bors r+
|
Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed `edge_symm` to `adj_comm`. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Build failed (retrying...): |
bors r- This needs a merge of master I think |
Canceled. |
@@ -97,21 +106,29 @@ instance complete_graph_adj_decidable (V : Type u) [decidable_eq V] : | |||
decidable_rel (complete_graph V).adj := | |||
λ v w, not.decidable | |||
|
|||
/-- The graph with no edges on a given vertex type `V`. -/ | |||
def empty_graph (V : Type u) : simple_graph V := | |||
{ adj := λ i j, false } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be a has_bot
instance?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
can also be has_top
with complete_graph
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@eric-wieser @ericrbg Yeah, and simple_graph
can be a bounded_lattice
. Would you mind if we held this off for another PR and merge this one?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've pushed a todo to remind us to do the work.
@hmonroe I think we're free to merge it now
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors r+
Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed `edge_symm` to `adj_comm`. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed `edge_symm` to `adj_comm`. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed
edge_symm
toadj_comm
.