R : Type ?u.72208
E : Type ?u.72211
F : Type ?u.72214
ι : Type ?u.72217
ι' : Type ?u.72220
α : Type ?u.72223
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
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ ∅ → 0 ≤ w i
hw₁ : 0 < ∑ i in ∅, w i
⊢ False
R : Type ?u.72208
E : Type ?u.72211
F : Type ?u.72214
ι : Type ?u.72217
ι' : Type ?u.72220
α : Type ?u.72223
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 ι
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : 0 < ∑ i in s, w i
⊢ s ≠ ∅
rintro rfl
no goals
R : Type ?u.72208
E : Type ?u.72211
F : Type ?u.72214
ι : Type ?u.72217
ι' : Type ?u.72220
α : Type ?u.72223
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
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ ∅ → 0 ≤ w i
hw₁ : 0 < ∑ i in ∅, w i
⊢ False
simp at hw₁
R : Type u_2
E : Type ?u.72211
F : Type ?u.72214
ι : Type u_1
ι' : Type ?u.72220
α : Type u_3
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 ι
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : 0 < ∑ i in s, w i
⊢ ∑ i in s, w i • f i ≤ ∑ i in s, w i • sup' s (_ : Finset.Nonempty s) f
R : Type u_2
E : Type ?u.72211
F : Type ?u.72214
ι : Type u_1
ι' : Type ?u.72220
α : Type u_3
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 ι
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : 0 < ∑ i in s, w i
⊢ centerMass s w f ≤ sup' s (_ : Finset.Nonempty s) f
rw [centerMass, inv_smul_le_iff hw₁, sum_smul]
no goals
R : Type u_2
E : Type ?u.72211
F : Type ?u.72214
ι : Type u_1
ι' : Type ?u.72220
α : Type u_3
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 ι
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : 0 < ∑ i in s, w i
⊢ ∑ i in s, w i • f i ≤ ∑ i in s, w i • sup' s (_ : Finset.Nonempty s) f
exact sum_le_sum fun i hi => smul_le_smul_of_nonneg (le_sup' _ hi) <| hw₀ i hi