no goals
𝕜 : Type u_1
𝕝 : Type ?u.72862
E : Type u_2
F : Type ?u.72868
β : Type ?u.72871
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)
simpa only [add_comm] using hs.preimage_add_right z