iSupIndep_of_dfinsupp_lsum_injective

English

If lsum restricted to each component is injective, then the family is iSupIndep.

Русский

Если отображение lsum по каждой компоненте инъективно, тогда семейство независимо по iSupIndep.

LaTeX

$$$iSupIndep p$ при условии инъективности $lsum \\dots$$$

Lean4

theorem iSupIndep_of_dfinsupp_lsum_injective (p : ι → Submodule R N)
    (h : Function.Injective (lsum ℕ fun i => (p i).subtype)) : iSupIndep p :=
  by
  rw [iSupIndep_iff_forall_dfinsupp]
  intro i x v hv
  replace hv : lsum ℕ (fun i => (p i).subtype) (erase i v) = lsum ℕ (fun i => (p i).subtype) (single i x) := by
    simpa only [lsum_single] using hv
  have := DFunLike.ext_iff.mp (h hv) i
  simpa [eq_comm] using this

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