no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.60058
β : Type ?u.60061
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x => x + z) ⁻¹' s)
simpa only [add_comm] using hs.translate_preimage_right z