memAddSubgroup — Mathlib

English

If D is in the additive subgroup of locally finite within U, then D as a function lies in that subgroup.

Русский

Если D принадлежит аддитивной подгруппе локально конечных внутри U, тогда D как функция находится в этой подгруппе.

LaTeX

$$D ∈ locallyFinsuppWithin.addSubgroup U$$

Lean4

protected theorem memAddSubgroup [AddCommGroup Y] (D : locallyFinsuppWithin U Y) :
    (D : X → Y) ∈ locallyFinsuppWithin.addSubgroup U :=
  ⟨D.supportWithinDomain, D.supportLocallyFiniteWithinDomain⟩

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