-
Notifications
You must be signed in to change notification settings - Fork 297
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.
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
[Merged by Bors] - feat(combinatorics/simple_graph/basic): introduce incidence sets, graph construction from relation #5191
Conversation
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
…ity/mathlib into simple_graphs3 grabbing commits from github
This looks great to me, except I note that |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
…ity/mathlib into simple_graphs3 implementing changes
I think the speed is reasonable, it only takes a few seconds at worst for proofs to work |
Keep in mind that mathlib has 40k+ theorems, so a few seconds for a proof is actually on the slower side of things. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ity/mathlib into simple_graphs3 pulling new commits
Is there anything else I should do here? |
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.
👍
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.
Otherwise LGTM. Thanks!
bors d+
✌️ agusakov can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors r+ |
…ph construction from relation (#5191) Add incidence sets and some lemmas, including a proof of equivalence between the neighbor set of a vertex and its incidence set. Add a graph construction from a given relation. Definitions and lemmas adapted from [simple_graphs2](https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/basic.lean#L317) Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>
Build failed: |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
…ity/mathlib into simple_graphs3 fixing proofs
bors r+ |
…ph construction from relation (#5191) Add incidence sets and some lemmas, including a proof of equivalence between the neighbor set of a vertex and its incidence set. Add a graph construction from a given relation. Definitions and lemmas adapted from [simple_graphs2](https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/basic.lean#L317) Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Add incidence sets and some lemmas, including a proof of equivalence between the neighbor set of a vertex and its incidence set. Add a graph construction from a given relation.
Definitions and lemmas adapted from simple_graphs2