eq_of_sum_eq_sum_subtype — Mathlib

English

There exists an affine independent subset t of s with the same affine span as s.

Русский

Существует аффинно независимое подмножество t внутри s, имеющее ту же оболочку, что и s.

LaTeX

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

Lean4

theorem eq_of_sum_eq_sum_subtype {s : Finset V} (hp : AffineIndependent k ((↑) : s → V)) {w₁ w₂ : V → k}
    (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i) : ∀ i ∈ s, w₁ i = w₂ i := by
  refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi) <;>
    simpa [sub_mul, sub_smul, sub_eq_zero]

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