Theorems · Theorem · geometry

AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} {p : ι → P},
  AffineIndependent k p →
    ∀ {s₁ : Finset ι} {s₂ : Finset ι₂} {w₁ : ι → k} {w₂ : ι₂ → k},
      ∑ i ∈ s₁, w₁ i = 1 →
        ∑ i ∈ s₂, w₂ i = 1 →
          ∀ (e : ι₂ ↪ ι),
            (Finset.affineCombination k s₂ (p ∘ ⇑e)) w₂ = (Finset.affineCombination k s₁ p) w₁ →
              (↑(Finset.map e s₂)).indicator (Function.extend (⇑e) w₂ 0) = (↑s₁).indicator w₁

Defined in

Mathlib.LinearAlgebra.AffineSpace.Independent

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsor