Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff #6157

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff #6157

wants to merge 12 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Jul 26, 2023 •
edited

Add if and only if versions of Monotone.dual and Antitone.dual.

Needed for #5672

Open in Gitpod

@mans0954 mans0954 added the awaiting-review The author would like community review of the PR label Jul 26, 2023
@mans0954 mans0954 mentioned this pull request Jul 26, 2023
Closed
2 tasks
ADedecker
ADedecker reviewed Jul 28, 2023
View reviewed changes
Copy link
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be nice to do the same for all the .dual lemma, and then remove them and use alias to get them from the iff versions. Could you please do that?

Mathlib/Order/Monotone/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Order/Monotone/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Order/Monotone/Basic.lean Outdated Show resolved Hide resolved
@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes t-order Order hierarchy and removed awaiting-review The author would like community review of the PR labels Jul 28, 2023
@mans0954 mans0954 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 28, 2023
@mans0954
Copy link
Collaborator Author

It would be nice to do the same for all the .dual lemma, and then remove them and use alias to get them from the iff versions. Could you please do that?

I think I've done this now.

ADedecker
ADedecker reviewed Jul 28, 2023
View reviewed changes
Mathlib/Order/Monotone/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Order/Monotone/Basic.lean Outdated
Comment on lines 243 to 244
alias monotone_dual_iff ↔ Monotone.dual _
#align monotone.dual Monotone.dual
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would be cleaner to move that below (with the other aliases), could you do that. Also, I've just realized this makes the names not protected anymore, which is annoying, so I asked on Zulip how can we go around that.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ADedecker I've moved the aliases - haven't seen a reply on Zulip about the protected names yet.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This feature indeed doesn't exist yet, but it will soon (leanprover-community/batteries#200). For now this doesn't cause any problems so I'll just merge it, we can add back protected later.

@ADedecker
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jul 31, 2023
bors bot pushed a commit that referenced this pull request Jul 31, 2023
@mans0954
feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_i…
c02f4f8 
…ff (#6157)

Add if and only if versions of `Monotone.dual` and `Antitone.dual`.

Needed for #5672



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
@bors
Copy link

bors bot commented Jul 31, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff [Merged by Bors] - feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff Jul 31, 2023
@bors bors bot closed this Jul 31, 2023
@bors bors bot deleted the mans0954/Monotone.dual_iff branch July 31, 2023 23:05
semorrison pushed a commit that referenced this pull request Aug 2, 2023
@mans0954 @semorrison
feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_i…
63f392a 
…ff (#6157)

Add if and only if versions of `Monotone.dual` and `Antitone.dual`.

Needed for #5672



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@mans0954 @semorrison
feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_i…
8564836 
…ff (#6157)

Add if and only if versions of `Monotone.dual` and `Antitone.dual`.

Needed for #5672



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ADedecker ADedecker ADedecker left review comments

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-order Order hierarchy
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@mans0954 @ADedecker