ι : Sort u_3
𝕜 : 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
s : ι → Set E
t : Set E
⊢ (⋃ (x : E) (i : ι) (_ : x ∈ s i) (y : E) (_ : y ∈ t), segment 𝕜 x y) =
    ⋃ (i : ι) (x : E) (_ : x ∈ s i) (y : E) (_ : y ∈ t), segment 𝕜 x y
ι : Sort u_3
𝕜 : 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
s : ι → Set E
t : Set E
⊢ convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t
simp_rw [convexJoin, mem_iUnion, iUnion_exists]
no goals
ι : Sort u_3
𝕜 : 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
s : ι → Set E
t : Set E
⊢ (⋃ (x : E) (i : ι) (_ : x ∈ s i) (y : E) (_ : y ∈ t), segment 𝕜 x y) =
    ⋃ (i : ι) (x : E) (_ : x ∈ s i) (y : E) (_ : y ∈ t), segment 𝕜 x y
exact iUnion_comm _