affineIndependent_def — Mathlib

English

Affine independence of p is equivalent to the property that any finite affine combination with zero total weight that yields the base point implies all weights are zero.

Русский

Аффинная независимость семейства точек эквивалентна тому, что любая аффинная линейная комбинация с суммой весов равной нулю, приводящая к базовой точке, обнуляет все веса.

LaTeX

$$$\text{AffineIndependent}_k(p) \iff \forall s,w, \sum_{i\in s} w_i = 0 \to s.weightedVSub p w = 0 \to \forall i\in s, w_i = 0$$$

Lean4

/-- The definition of `AffineIndependent`. -/
theorem affineIndependent_def (p : ι → P) :
    AffineIndependent k p ↔
      ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0 :=
  Iff.rfl

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