[Merged by Bors] - feat: Extending convex functions #6339
Conversation
YaelDillies
added
awaiting-review
mathlib3-pair
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
Mathlib/Analysis/Convex/ProjIcc.lean
Outdated
| @@ -0,0 +1,99 @@ | |||
| /- | |||
There was a problem hiding this comment.
This file is new, right? If so, can you drop it from this PR so that it can be reviewed as a port, not a forward-port?
There was a problem hiding this comment.
This file is a forward-port, though?
There was a problem hiding this comment.
It's only a forward-port if it's a modification of a file that was already ported from the out-of-sync region of https://leanprover-community.github.io/mathlib-port-status; otherwise it's just a sparkling port.
It's best to do this in a separate PR using start_port.sh so that the review against mathport is possible. Obviously that will have to wait for the rest of this files in this PR to be merged first.
There was a problem hiding this comment.
Did you recently change the presentation of out-of-sync? I swear I copied that code from there 🤔
YaelDillies
removed
the
merge-conflict
| @@ -64,6 +64,7 @@ variable [Preorder α] [Preorder β] | |||
| theorem Monotone.image_Icc_subset (h : Monotone f) : | |||
| f '' Icc a b ⊆ Icc (f a) (f b) := | |||
| h.mapsTo_Icc.image_subset | |||
| #align monotone.image_Icc_subset Monotone.image_Icc_subset | |||
There was a problem hiding this comment.
Where are the other three lemmas, MonotoneOn.image_Icc_subset, AntitoneOn.image_Icc_subset, and Antitone.image_Icc_subset? I'm a bit confused, because your previous version had maybe 20 new lemmas, but this one is now missing 3 lemmas.
There was a problem hiding this comment.
Two approaches come to mind:
- Add
#noaligns for the other three lemmas with a TODO comment - Make a separate PR that adds this whole family of lemmas (first), then update this one to just add the aligns.
There was a problem hiding this comment.
Went for the second because it's less work for me: #7146.
bors
bot
changed the base branch from
master
to
ScottCarnahan/BinomialRing2
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
bors d+ I think I finished this us, please merge if it looks good to you and CI. |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thank you for the merge. bors merge |
Forward-ports leanprover-community/mathlib3#18797 The changes to `Mathlib.Data.Set.Intervals.Basic` were independently added to mathlib4 in `Mathlib.Data.Set.Intervals.Image`, so the `#align`s have been added there instead of the original file. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Build failed: |
|
"No space left on device". I'll rerun bors once this is fixed: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/No.20space.20left.20on.20device |
|
Hopefully fixed now. bors merge |
Forward-ports leanprover-community/mathlib3#18797 The changes to `Mathlib.Data.Set.Intervals.Basic` were independently added to mathlib4 in `Mathlib.Data.Set.Intervals.Image`, so the `#align`s have been added there instead of the original file. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
This PR was included in a batch that was canceled, it will be automatically retried |
Forward-ports leanprover-community/mathlib3#18797 The changes to `Mathlib.Data.Set.Intervals.Basic` were independently added to mathlib4 in `Mathlib.Data.Set.Intervals.Image`, so the `#align`s have been added there instead of the original file. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Forward-ports leanprover-community/mathlib3#18797
The changes to
Mathlib.Data.Set.Intervals.Basicwere independently added to mathlib4 inMathlib.Data.Set.Intervals.Image, so the#aligns have been added there instead of the original file.This does not quite match the mathlib PR since Scott independently proved
Monotone.image_Icc_subsetin a new file. So instead of porting those changes, I'm integrating them to Scott's new file.