R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ centerMass s (fun i => w i) v ∈ ↑(convexHull R).toOrderHom (Set.range v)
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ ↑(affineCombination R s v) w ∈ ↑(convexHull R).toOrderHom (Set.range v)
rw [affineCombination_eq_centerMass hw₁]
case hws
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ 0 < ∑ i in s, w i

case hz
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ ∀ (i : ι), i ∈ s → v i ∈ Set.range v
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ centerMass s (fun i => w i) v ∈ ↑(convexHull R).toOrderHom (Set.range v)
apply s.centerMass_mem_convexHull hw₀
no goals
case hws
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ 0 < ∑ i in s, w i
simp [hw₁]
no goals
case hz
R : Type u_2
E : Type u_3
F : Type ?u.131675
ι : Type u_1
ι' : Type ?u.131681
α : Type ?u.131684
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ ∀ (i : ι), i ∈ s → v i ∈ Set.range v
simp