[Merged by Bors] - feat(analysis/complex/basic): convex_on.sup

[pechersky]

---

• depends on: [Merged by Bors] - chore(analysis/convex/basic): generalize concave_on.le_on_segment to monoids #8959

[YaelDillies]

As long as you're there, maybe be cautious and add the TODO explaining how to relax the typeclasses (if you have already figured it out?).

Have we defined has_Inf (α → β) when has_Inf β? If so, you might as well prove convex_on.Sup and convex_on.Inf, even though I think has_Inf γ along with the current assumption ordered_module ℝ γ imply subsingleton γ.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - chore(analysis/convex/basic): generalize concave_on.le_on_segment to monoids #8959

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[pechersky]

As long as you're there, maybe be cautious and add the TODO explaining how to relax the typeclasses (if you have already figured it out?).

Have we defined has_Inf (α → β) when has_Inf β? If so, you might as well prove convex_on.Sup and convex_on.Inf, even though I think has_Inf γ along with the current assumption ordered_module ℝ γ imply subsingleton γ.

With the generalization PR in master, I can place it in the right generalization level now.

[eric-wieser]

LGTM

bors d=@YaelDillies

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

LGTM

bors d=@YaelDillies

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

This looks all good! I'll PR convex_on.Sup and convex_on.Inf myself.
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests