R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
⊢ ∑ x in t, (∑ x in t', w x)⁻¹ • w x • z x = ∑ x in t', (∑ i in t', w i)⁻¹ • w x • z x
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
⊢ centerMass t w z = centerMass t' w z
rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
⊢ ∀ (x : ι), x ∈ t' → ¬x ∈ t → (∑ x in t', w x)⁻¹ • w x • z x = 0
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
⊢ ∑ x in t, (∑ x in t', w x)⁻¹ • w x • z x = ∑ x in t', (∑ i in t', w i)⁻¹ • w x • z x
apply sum_subset ht
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
i : ι
hit' : i ∈ t'
hit : ¬i ∈ t
⊢ (∑ x in t', w x)⁻¹ • w i • z i = 0
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
⊢ ∀ (x : ι), x ∈ t' → ¬x ∈ t → (∑ x in t', w x)⁻¹ • w x • z x = 0
intro i hit' hit
no goals
R : Type u_2
E : Type u_3
F : Type ?u.65551
ι : Type u_1
ι' : Type ?u.65557
α : Type ?u.65560
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ (i : ι), i ∈ t' → ¬i ∈ t → w i = 0
i : ι
hit' : i ∈ t'
hit : ¬i ∈ t
⊢ (∑ x in t', w x)⁻¹ • w i • z i = 0
rw [h i hit' hit, zero_smul, smul_zero]