-
Notifications
You must be signed in to change notification settings - Fork 259
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: Simple graphs form a complete boolean algebra #2502
Conversation
4aa0f2f
to
dcba322
Compare
I just spent two hours trying to fix the errors, but VScode isn't cooperating. If you try fixing it, know that everything broke because |
…lib4 into simple_graph_complete_boolean_algebra
I went through leanprover-community/mathlib#18285 line by line to check that this PR is making all the same changes, and I also fixed the rest of the errors. I did cheat with some of the proofs and rewrote them using |
I went through your changes and I'm very happy with your new proofs! 🙏 |
bors merge |
Match leanprover-community/mathlib#18285 * [`combinatorics.simple_graph.basic`@`db53863fb135228820ee0b08e8dce9349a3d911b`..`c6ef6387ede9983aee397d442974e61f89dfd87b`](https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/simple_graph/basic?range=db53863fb135228820ee0b08e8dce9349a3d911b..c6ef6387ede9983aee397d442974e61f89dfd87b) * [`combinatorics.simple_graph.subgraph`@`d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80`..`c6ef6387ede9983aee397d442974e61f89dfd87b`](https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/simple_graph/subgraph?range=d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80..c6ef6387ede9983aee397d442974e61f89dfd87b) Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Match leanprover-community/mathlib#18285 * [`combinatorics.simple_graph.basic`@`db53863fb135228820ee0b08e8dce9349a3d911b`..`c6ef6387ede9983aee397d442974e61f89dfd87b`](https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/simple_graph/basic?range=db53863fb135228820ee0b08e8dce9349a3d911b..c6ef6387ede9983aee397d442974e61f89dfd87b) * [`combinatorics.simple_graph.subgraph`@`d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80`..`c6ef6387ede9983aee397d442974e61f89dfd87b`](https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/simple_graph/subgraph?range=d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80..c6ef6387ede9983aee397d442974e61f89dfd87b) Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Match leanprover-community/mathlib#18285
combinatorics.simple_graph.basic
@db53863fb135228820ee0b08e8dce9349a3d911b
..c6ef6387ede9983aee397d442974e61f89dfd87b
combinatorics.simple_graph.subgraph
@d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80
..c6ef6387ede9983aee397d442974e61f89dfd87b