𝕜 : Type u_1
E : Type u_2
F : Type ?u.537715
α : Type ?u.537718
β : Type u_3
ι : Type ?u.537724
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.537715
α : Type ?u.537718
β : Type u_3
ι : Type ?u.537724
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y
rw [add_comm] at hab hfx⊢
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.537715
α : Type ?u.537718
β : Type u_3
ι : Type ?u.537724
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y
exact hf.le_left_of_right_le' hy hx hb ha hab hfx