linearIndependent_iff'ₛ — Mathlib

English

Another Finset-based equivalence, expressing independence in terms of Finset-labeled sums equality implies coefficient equality.

Русский

Ещё одно эквивалентное формулирование через Finset: равенство линейных комбинаций по Finset влечёт равенство коэффициентов.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\iff \\forall s:\\operatorname{Finset} ι, \\forall f,g:ι→R, (\\sum_{i∈s} f_i v_i)=(\\sum_{i∈s} g_i v_i) → \\forall i∈s, f_i=g_i$$$

Lean4

theorem linearIndependent_iff'ₛ :
    LinearIndependent R v ↔
      ∀ s : Finset ι, ∀ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i :=
  linearIndependent_iffₛ.trans
    ⟨fun hv s f g eq i his ↦
      by
      have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
      have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i)) := by {
            rw [Finsupp.lapply_apply, Finsupp.single_eq_same]
          }
          _ = ∑ j ∈ s, (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single j (f j)) :=
            (Eq.symm <|
              Finset.sum_eq_single i (fun j _hjs hji => by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji])
                fun hnis => hnis.elim his)
          _ = (∑ j ∈ s, Finsupp.single j (f j)) i := (map_sum ..).symm
      rw [this f, this g, h], fun hv f g hl ↦
      Finsupp.ext fun _ ↦ by
        classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        ·
          rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;> rintro i - hi <;>
            rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
        · contrapose! hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.2]⟩

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