no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.716463
α : Type ?u.716466
β : Type u_3
ι : Type ?u.716472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCancelCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c : E
⊢ StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
simpa only [add_comm] using hf.translate_right c