no goals
ι : Sort ?u.16420
𝕜 : Type u_2
E : Type u_1
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t✝ s₁ s₂ t₁ t₂ u : Set E
x y : E
t : Set E
⊢ convexJoin 𝕜 ∅ t = ∅
simp [convexJoin]