𝕜 : Type u_2
E : Type u_1
F : Type ?u.23294
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ {x, y} ⊆ segment 𝕜 x y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.23294
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ ↑(convexHull 𝕜).toOrderHom {x, y} = segment 𝕜 x y
refine (convexHull_min ?_ <| convex_segment _ _).antisymm
  (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.23294
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.23294
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ {x, y} ⊆ segment 𝕜 x y
rw [insert_subset, singleton_subset_iff]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.23294
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩