linearIndepOn_iffₛ — Mathlib

English

Characterizations of independence via Finset on s, using finite sums and uniqueness of coefficients.

Русский

Характеризации независимости через конечные подмножества, используя конечные суммы и уникальность коэффициентов.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R v s \\\\iff \\\\forall f \\in \\mathrm{Finsupp} s R, \\forall g \\in \\mathrm{Finsupp} s R, \\\\text{linearCombination } R v f = \\text{linearCombination } R v g \\\\Rightarrow f=g.$$$

Lean4

theorem linearIndepOn_iffₛ :
    LinearIndepOn R v s ↔
      ∀ f ∈ Finsupp.supported R R s,
        ∀ g ∈ Finsupp.supported R R s, Finsupp.linearCombination R v f = Finsupp.linearCombination R v g → f = g :=
  by
  simp only [LinearIndepOn, linearIndependent_iffₛ, Finsupp.mem_supported, Finsupp.linearCombination_apply,
    Set.subset_def, Finset.mem_coe]
  refine
    ⟨fun h l₁ h₁ l₂ h₂ eq ↦
      (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <|
        h _ _ <| (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
      fun h l₁ l₂ eq ↦ ?_⟩
  refine Finsupp.embDomain_injective (Embedding.subtype s) <| h _ ?_ _ ?_ ?_
  iterate 2 simpa using fun _ h _ ↦ h
  simp_rw [Finsupp.embDomain_eq_mapDomain]
  rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index] <;> intros <;> simp only [zero_smul, add_smul]

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