intro b
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
⊢ QuasiconvexOn 𝕜 t f
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ f x ≤ b}