no goals
𝕜 : Type u_2
E : Type u_4
F : Type u_1
α : Type ?u.262486
β : Type u_3
ι : Type ?u.262492
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : OrderedAddCommMonoid α
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] F
x : E
hx : x ∈ ↑g ⁻¹' s
y : E
hy : y ∈ ↑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (↑g (a • x + b • y)) = f (a • ↑g x + b • ↑g y)
rw [g.map_add, g.map_smul, g.map_smul]