no goals
𝕜 : Type ?u.61842
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : ¬x ∈ t
f : E →L[ℝ] ℝ
hf : ∀ (a : E), a ∈ t → ↑f a < ↑f x
⊢ ∀ (b : E), b ∈ t → ↑(-f) x < ↑(-f) b
simpa