[Merged by Bors] - feat(data/set/intervals/proj_Icc): Extending from Ici a#18795
[Merged by Bors] - feat(data/set/intervals/proj_Icc): Extending from Ici a#18795YaelDillies wants to merge 4 commits intomasterfrom
Ici a#18795Conversation
| variables [preorder β] {a b : α} (h : a ≤ b) {f : Icc a b → β} | ||
| variables [preorder β] {s t : set α} {a b : α} (h : a ≤ b) {f : Icc a b → β} | ||
|
|
||
| protected lemma monotone.Ici_extend {f : Ici a → β} (hf : monotone f) : monotone (Ici_extend f) := |
There was a problem hiding this comment.
should these sorts of lemmas be tagged @[mono]?
There was a problem hiding this comment.
Can @[mono] deal with lemmas that have assumptions?
There was a problem hiding this comment.
Really unsure...
There was a problem hiding this comment.
Did you try it in some example?
|
LGTM. Please add a comment about future applications of new definitions to the commit message. Thanks! |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Unblocked now bors merge |
|
Build failed: |
|
bors merge |
|
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. |
Ici aIci a
leanprover-community/mathlib3#18795 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community/mathlib3#18795 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community/mathlib3#18795 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Define the
IciandIicversions ofset.proj_Icc/set.Icc_extend. Slightly reorder the lemmas to allow better overall structure.This is useful for extending convex functions by a junk value.