eq_zero_of_sum_eq_zero_subtype — Mathlib

English

Any affinely independent set can be extended to a subset whose affine span is the whole space.

Русский

Любое аффинно независимое множество можно дополнить до подмножества, чья аффинная оболочка равна всему пространству.

LaTeX

$$$\\exists t\\subseteq s,\\; \\mathrm{affineSpan}_k(t)=\\mathrm{affineSpan}_k(s)\\; \\wedge\\; \\operatorname{AffineIndependent} k \\big(\\mathrm{incl} : t\\to P\\big)$$$

Lean4

theorem eq_zero_of_sum_eq_zero_subtype {s : Finset V} (hp : AffineIndependent k ((↑) : s → V)) {w : V → k}
    (hw₀ : ∑ x ∈ s, w x = 0) (hw₁ : ∑ x ∈ s, w x • x = 0) : ∀ x ∈ s, w x = 0 :=
  by
  rw [← sum_attach] at hw₀ hw₁
  exact fun x hx ↦ hp.eq_zero_of_sum_eq_zero hw₀ hw₁ ⟨x, hx⟩ (mem_univ _)

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