Theorems · Theorem · geometry

Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {v : V} {x : k} {s : Set ι} {p : ι → P} {b : P},
  (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i => p ↑i) b) w

Suppose an indexed family of points is given, along with a subset of the index type. A vector can be expressed as weightedVSubOfPoint using a Finset lying within that subset and with a given sum of weights if and only if it can be expressed as weightedVSubOfPoint with that sum of weights for the corresponding indexed family whose index type is the subtype corresponding to that subset.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

2 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor