indicator_eq_of_affineCombination_eq

English

Affine independence implies that equal affine combinations yield equal indicator functions.

Русский

Аффинная независимость подразумевает равенство индикаторов при равенстве аффинных комбинаций.

LaTeX

$$AffineIndependent k p → ∀ s1 s2 w1 w2, ∑ i∈s1 w1 i = 1 → ∑ i∈s2 w2 i = 1 → s1.affineCombination k p w1 = s2.affineCombination k p w2 → Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2$$

Lean4

theorem indicator_eq_of_affineCombination_eq {p : ι → P} (ha : AffineIndependent k p) (s₁ s₂ : Finset ι) (w₁ w₂ : ι → k)
    (hw₁ : ∑ i ∈ s₁, w₁ i = 1) (hw₂ : ∑ i ∈ s₂, w₂ i = 1)
    (h : s₁.affineCombination k p w₁ = s₂.affineCombination k p w₂) : Set.indicator (↑s₁) w₁ = Set.indicator (↑s₂) w₂ :=
  (affineIndependent_iff_indicator_eq_of_affineCombination_eq k p).1 ha s₁ s₂ w₁ w₂ hw₁ hw₂ h

Похожие утверждения