def subsetSums {M : Type u_1} [AddCommMonoid M] (A : Set M) : Set M

The set of subset sums of a set A ⊆ M.

Equations

• subsetSums A = {n : M | ∃ (B : Finset M), ↑B ⊆ A ∧ n = ∑ i ∈ B, i}

def subseqSums {M : Type u_1} [AddCommMonoid M] (A : ℕ → M) : Set M

The set of subset sums of a sequence ℕ → M.

Equations

• subseqSums A = {n : M | ∃ (B : Finset ℕ), Set.InjOn A ↑B ∧ n = ∑ i ∈ B, A i}

def subseqSums' {M : Type u_1} [AddCommMonoid M] (A : ℕ → M) : Set M

The set of subset sums of a sequence ℕ → M, where repetition is allowed.

Equations

• subseqSums' A = {n : M | ∃ (B : Finset ℕ), n = ∑ i ∈ B, A i}

def IsAddComplete {M : Type u_1} [AddCommMonoid M] [Preorder M] (A : Set M) : Prop

A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A.

Equations

• IsAddComplete A = ∀ᶠ (k : M) in Filter.atTop, k ∈ subsetSums A

def IsAddCompleteNatSeq {M : Type u_1} [AddCommMonoid M] [Preorder M] (A : ℕ → M) : Prop

A sequence A is complete if every sufficiently large element of M is a sum of distinct terms of A.

Equations

• IsAddCompleteNatSeq A = ∀ᶠ (k : M) in Filter.atTop, k ∈ subseqSums A

def IsAddCompleteNatSeq' {M : Type u_1} [AddCommMonoid M] [Preorder M] (A : ℕ → M) : Prop

A sequence A is complete if every sufficiently large element of M is a sum of (not necessarily distinct) terms of A.

Equations

• IsAddCompleteNatSeq' A = ∀ᶠ (k : M) in Filter.atTop, k ∈ subseqSums' A