feat(analysis/convex/basic): add lemmas about convex combination of endpoints of intervals (#3482)
feat(analysis/convex/basic): add lemmas about convex combination of endpoints of intervals (#3482)



Co-authored-by: Frédéric Dupuis <85fbb02ca4514343a46329a92ab18d1dede56561@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib