𝕜 : Type u_1
E : Type u_2
F : Type ?u.4373
β : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
𝕜 : Type u_1
E : Type u_2
F : Type ?u.4373
β : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
⊢ QuasiconvexOn 𝕜 s (f ⊔ g)
intro r
𝕜 : Type u_1
E : Type u_2
F : Type ?u.4373
β : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})
𝕜 : Type u_1
E : Type u_2
F : Type ?u.4373
β : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.4373
β : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})
exact (hf r).inter (hg r)