English
Duplicate of the finite index set version illustrating the connection with Finset sums.
Русский
Дубликат версии с конечным набором индексов, иллюстрирующий связь с суммами по Finset.
LaTeX
$$$(a \\in iSup fun i \\in s => p_i) \\iff \\exists \\mu, \\sum_{i \\in s} \\mu_i = a$$$
Lean4
/-- Independence of a family of submodules can be expressed as a quantifier over `DFinsupp`s.
This is an intermediate result used to prove
`iSupIndep_of_dfinsupp_lsum_injective` and
`iSupIndep.dfinsupp_lsum_injective`. -/
theorem iSupIndep_iff_forall_dfinsupp (p : ι → Submodule R N) :
iSupIndep p ↔ ∀ (i) (x : p i) (v : Π₀ i : ι, ↥(p i)), lsum ℕ (fun i => (p i).subtype) (erase i v) = x → x = 0 :=
by
simp_rw [iSupIndep_def, Submodule.disjoint_def, Submodule.mem_biSup_iff_exists_dfinsupp, exists_imp,
filter_ne_eq_erase]
refine forall_congr' fun i => Subtype.forall'.trans ?_
simp_rw [Submodule.coe_eq_zero]
/- If `DFinsupp.lsum` applied with `Submodule.subtype` is injective then the submodules are
iSupIndep. -/
