no goals
ι : Sort ?u.1646
𝕜 : 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
⊢ x ∈ convexJoin 𝕜 s t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ x ∈ segment 𝕜 a b
simp [convexJoin]