no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.180457
β : Type ?u.180460
inst✝⁴ : OrderedCommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
z : E
c : 𝕜
⊢ Convex 𝕜 ((fun x => z + c • x) '' s)
simpa only [← image_smul, ← image_vadd, image_image] using (hs.smul c).vadd z