no goals
ι : Sort ?u.27529
𝕜 : 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
s : Set E
y : E
⊢ convexJoin 𝕜 s {y} = ⋃ (x : E) (_ : x ∈ s), segment 𝕜 x y
simp [convexJoin]