English
If s and t are disjoint subsets of an index set and f: index → M is a family, then linear independence on s ∪ t follows from linear independence on s and independence of the quotient copy on t.
Русский
Если s и t — попарно непересекающиеся подмножества множества индексов и f: индексы → M представляет семейство, то линейная независимость на s ∪ t следует из независимости на s и независимости по копии в реляции через фактор-множество на t.
LaTeX
$$$\text{LinearIndepOn}_R f (s \cup t) \,\text{(из условий на }s,t\text{)}$$$
Lean4
theorem sumElim_of_quotient {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M)
(hg : LinearIndependent R (Submodule.Quotient.mk (p := M') ∘ g)) :
LinearIndependent R (Sum.elim (f · : ι₁ → M) g) :=
by
refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this
rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]
