addSubmonoid_iSupIndep — Mathlib

English

If A_i are iSupIndep, then DirectSum.IsInternal (i ↦ (A_i).comap (iSup ...).subtype) holds; i.e., the direct-sum comaps form an internal family.

Русский

Если A_i образуют iSupIndep, тогда DirectSum.IsInternal (i ↦ (A_i).comap …) выполняется; результат — внутренняя совокупность подмножеств в прямой сумме.

LaTeX

$$$iSupIndep\big(\lambda i:\, i, A i\big) \to IsInternal\big(\lambda i:\, s \mapsto (A i).comap (iSup (\lambda h, A h)).subtype\big)$$$

Lean4

theorem addSubmonoid_iSupIndep {M : Type*} [AddCommMonoid M] {A : ι → AddSubmonoid M} (h : IsInternal A) :
    iSupIndep A :=
  iSupIndep_of_dfinsuppSumAddHom_injective _ h.injective

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