Theorems · Theorem · geometry

Finset.eq_affineCombination_subset_iff_eq_affineCombination_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} {p0 : P} {s : Set ι} {p : ι → P},
  (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs fun i => p ↑i) w

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

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsor