ι : Sort ?u.66107
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ u✝ : Set E
x y : E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
ι : Sort ?u.66107
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ u✝ : Set E
x y : E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)
refine' (convexJoin_assoc_aux _ _ _).antisymm _
ι : Sort ?u.66107
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ u✝ : Set E
x y : E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
ι : Sort ?u.66107
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ u✝ : Set E
x y : E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
simp_rw [convexJoin_comm s, convexJoin_comm _ u]
no goals
ι : Sort ?u.66107
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ u✝ : Set E
x y : E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
exact convexJoin_assoc_aux _ _ _