k : Type u_3
V : Type u_2
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.58761
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i in s₁, w i • (p i -ᵥ b) = ∑ i in s₂, Set.indicator (↑s₁) w i • (p i -ᵥ b)
k : Type u_3
V : Type u_2
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.58761
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ↑(weightedVSubOfPoint s₁ p b) w = ↑(weightedVSubOfPoint s₂ p b) (Set.indicator (↑s₁) w)
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
no goals
k : Type u_3
V : Type u_2
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.58761
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i in s₁, w i • (p i -ᵥ b) = ∑ i in s₂, Set.indicator (↑s₁) w i • (p i -ᵥ b)
exact
  Set.sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _