English
For an affine independent p, if two affine combinations have equal sums and evaluate to the same point, then their indicators are equal.
Русский
Для аффинно независимого p, если две аффинные комбинации имеют одинаковые суммы и дают одно и то же значение, то индикация равна.
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
/-- An affinely independent family is injective, if the underlying
ring is nontrivial. -/
protected theorem injective [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) : Function.Injective p :=
by
intro i j hij
rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha
by_contra hij'
refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)
simp_all only [ne_eq]
