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