iSupIndep_of_dfinsuppSumAddHom_injective

English

If the sumAddHom induced map is injective, then iSupIndep for the dfinsupp family holds.

Русский

Если отображение sumAddHom инъективно, то выполняется iSupIndep для данной dfinsupp семьи.

LaTeX

$$$iSupIndep(p)$ через инъекцию sumAddHom$$$

Lean4

theorem iSupIndep_of_dfinsuppSumAddHom_injective (p : ι → AddSubmonoid N)
    (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p :=
  by
  rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

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