Theorems · Theorem · geometry

Finset.affineCombination_indicator_subset

∀ {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} (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι},
  s₁ ⊆ s₂ → (Finset.affineCombination k s₁ p) w = (Finset.affineCombination k s₂ p) ((↑s₁).indicator w)

An affine combination is unaffected by changing the weights to the corresponding indicator function and adding points to the set.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Combination

Cited by

11 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsor