ι : Sort ?u.132103
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x y : E
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ↑(convexHull 𝕜).toOrderHom (↑(convexHull 𝕜).toOrderHom s ∪ ↑(convexHull 𝕜).toOrderHom t) =
    convexJoin 𝕜 (↑(convexHull 𝕜).toOrderHom s) (↑(convexHull 𝕜).toOrderHom t)
ι : Sort ?u.132103
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x y : E
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ↑(convexHull 𝕜).toOrderHom (s ∪ t) = convexJoin 𝕜 (↑(convexHull 𝕜).toOrderHom s) (↑(convexHull 𝕜).toOrderHom t)
rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]
no goals
ι : Sort ?u.132103
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x y : E
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ↑(convexHull 𝕜).toOrderHom (↑(convexHull 𝕜).toOrderHom s ∪ ↑(convexHull 𝕜).toOrderHom t) =
    convexJoin 𝕜 (↑(convexHull 𝕜).toOrderHom s) (↑(convexHull 𝕜).toOrderHom t)
exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull