no goals
ι : Sort ?u.34631
𝕜 : 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 x : E
⊢ convexJoin 𝕜 {x} {y} = segment 𝕜 x y
simp