k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s✝ : Finset ι
ι₂ : Type ?u.394352
s₂ : Finset ι₂
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs h w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) = ↑(weightedVSubOfPoint fs p (Classical.choice (_ : Nonempty P))) w) ↔
    ∃ fs w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) =
        ↑(weightedVSubOfPoint fs (fun i => p ↑i) (Classical.choice (_ : Nonempty P))) w
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s✝ : Finset ι
ι₂ : Type ?u.394352
s₂ : Finset ι₂
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs x w x, p0 = ↑(affineCombination k fs p) w) ↔ ∃ fs w x, p0 = ↑(affineCombination k fs fun i => p ↑i) w
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]
no goals
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s✝ : Finset ι
ι₂ : Type ?u.394352
s₂ : Finset ι₂
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs h w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) = ↑(weightedVSubOfPoint fs p (Classical.choice (_ : Nonempty P))) w) ↔
    ∃ fs w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) =
        ↑(weightedVSubOfPoint fs (fun i => p ↑i) (Classical.choice (_ : Nonempty P))) w
exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype