{calc
  f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
  _ ≤ a • r + b • r :=
    (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
  _ = r := Convex.combo_self hab r
}
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
no goals