Skip to content

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

Closed
mans0954 wants to merge 12 commits intomasterfrom
mans0954/Monotone.dual_iff
Closed

[Merged by Bors] - feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff#6157
mans0954 wants to merge 12 commits intomasterfrom
mans0954/Monotone.dual_iff

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Jul 26, 2023 •
edited
Loading

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

Needed for #5672

Open in Gitpod

@mans0954 mans0954 mentioned this pull request Jul 26, 2023
Closed
2 tasks
ADedecker
ADedecker reviewed Jul 28, 2023
View reviewed changes
Copy link
Copy Markdown
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?

@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes. t-order Order theory and removed awaiting-review labels Jul 28, 2023
@mans0954 mans0954 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 28, 2023
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jul 28, 2023

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
Comment on lines 243 to 244
alias monotone_dual_iff ↔ Monotone.dual _
#align monotone.dual Monotone.dual
Copy link
Copy Markdown
Member

@ADedecker ADedecker Jul 28, 2023

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
Copy Markdown
Collaborator Author

@mans0954 mans0954 Jul 30, 2023

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
Copy Markdown
Member

@ADedecker ADedecker Jul 31, 2023

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
Copy Markdown
Member

ADedecker commented Jul 31, 2023

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review 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
Copy Markdown

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
kim-em pushed a commit that referenced this pull request Aug 2, 2023
@mans0954 @kim-em
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>
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@mans0954 @kim-em
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 theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mans0954 @ADedecker