no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.650858
α : Type ?u.650861
β : Type u_3
ι : Type ?u.650867
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f g : E → β
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
rw [← neg_convexOn_iff, neg_neg f]