[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
hmonroe
added
the
awaiting-review
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 |
github-actions
bot
added
delegated
|
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.
Should this be a has_bot instance?
There was a problem hiding this comment.
can also be has_top with complete_graph
There was a problem hiding this comment.
@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.
I've pushed a todo to remind us to do the work.
@hmonroe I think we're free to merge it now
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: |
bors
bot
changed the title
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_symmtoadj_comm.