affineIndependent_vadd — Mathlib

English

Affine independence of a family is preserved under translation by a fixed vector v ∈ V.

Русский

Аффинально независимое семейство сохраняет аффинную независимость при сдвиге на фиксированный вектор v ∈ V.

LaTeX

$$$\text{AffineIndependent}_k(v +\!_V p) \iff \text{AffineIndependent}_k(p)$$$

Lean4

@[simp]
theorem affineIndependent_vadd {p : ι → P} {v : V} : AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p := by
  simp +contextual [AffineIndependent, weightedVSub_vadd]

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