-
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] - chore(data/set/pairwise): split #17880
Conversation
`finset.disj_Union` is not used in most of mathlib. This PR move most of related things into a new file. This PR also move other things about `set.pairwise` in `data.finset.basic` into `data.finset.pairwise`.
This PR moves some lemmas in `data.set.lattice` to `data.set.basic`, `data.set.image`, and `data.set.function`. They are basic enough and do not depend on the set lattice. This also helps #17880 to split `data.set.pairwise` and reduce the dependency of many files. mathlib4 PR: leanprover-community/mathlib4#1109
This PR/issue depends on: |
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.
Thanks. This is a sensible split. Could you fix the conflict?
For delegation,
maintainer merge
The conflict vanished. maintainer merge |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
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.
Thanks!
bors r+
This PR will split most of the lemmas in `data.set.pairwise` which are independent of the `data.set.lattice`. It makes a lot of files no longer depend on `data.set.lattice`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/315072418) mathlib4 PR: leanprover-community/mathlib4#1184 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed (retrying...): |
This PR will split most of the lemmas in `data.set.pairwise` which are independent of the `data.set.lattice`. It makes a lot of files no longer depend on `data.set.lattice`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/315072418) mathlib4 PR: leanprover-community/mathlib4#1184 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed: |
I'm not sure why Bors says it's a linting error and GitHub a build error... bors d+ |
✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
This PR will split most of the lemmas in `data.set.pairwise` which are independent of the `data.set.lattice`. It makes a lot of files no longer depend on `data.set.lattice`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/315072418) mathlib4 PR: leanprover-community/mathlib4#1184 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
alias function.injective_iff_pairwise_ne ↔ function.injective.pairwise_ne _ | ||
|
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.
What happened to this alias?
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.
It is already declared in logic.pairwise
. cf the porting note in mathlib4.
Match leanprover-community/mathlib#17880 The new import of `Mathlib.Data.Set.Lattice` in `Mathlib.Data.Finset.Basic` was implied transitively from tactic imports present in Lean 3. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Match leanprover-community/mathlib#17880 The new import of `Mathlib.Data.Set.Lattice` in `Mathlib.Data.Finset.Basic` was implied transitively from tactic imports present in Lean 3. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
This PR will split most of the lemmas in
data.set.pairwise
which are independent of thedata.set.lattice
. It makes a lot of files no longer depend ondata.set.lattice
.Zulip
mathlib4 PR: leanprover-community/mathlib4#1184