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 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