ι : Type u_2
ι' : Type ?u.89155
E : Type u_1
F : Type ?u.89161
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
ι : Type u_2
ι' : Type ?u.89155
E : Type u_1
F : Type ?u.89161
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ Convex ℝ (parallelepiped v)
rw [parallelepiped_eq_sum_segment]
ι : Type u_2
ι' : Type ?u.89155
E : Type u_1
F : Type ?u.89161
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : AddSubmonoid (Set E) :=
  {
    toAddSubsemigroup :=
      { carrier := {s | Convex ℝ s}, add_mem' := (_ : ∀ {a b : Set E}, Convex ℝ a → Convex ℝ b → Convex ℝ (a + b)) },
    zero_mem' := (_ : Convex ℝ {0}) }
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
ι : Type u_2
ι' : Type ?u.89155
E : Type u_1
F : Type ?u.89161
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
let A : AddSubmonoid (Set E) :=
  { carrier := { s | Convex ℝ s }
    zero_mem' := convex_singleton _
    add_mem' := Convex.add }
no goals
ι : Type u_2
ι' : Type ?u.89155
E : Type u_1
F : Type ?u.89161
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : AddSubmonoid (Set E) :=
  {
    toAddSubsemigroup :=
      { carrier := {s | Convex ℝ s}, add_mem' := (_ : ∀ {a b : Set E}, Convex ℝ a → Convex ℝ b → Convex ℝ (a + b)) },
    zero_mem' := (_ : Convex ℝ {0}) }
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
refine A.sum_mem (fun i _hi => convex_segment _ _)