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}

theorem subsetSums_mono {M : Type u_1} [AddCommMonoid M] {A B : Set M} (h : A ⊆ B) : subsetSums A ⊆ subsetSums B

If A ⊆ B, then subsetSums A ⊆ subsetSums B.

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

theorem IsAddComplete.mono {M : Type u_1} [AddCommMonoid M] [Preorder M] {A B : Set M} (h : A ⊆ B) (ha : IsAddComplete A) : IsAddComplete B

If A ⊆ B and A is complete, then B is also complete.

def IsAddStronglyComplete {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

• IsAddStronglyComplete A = ∀ ⦃B : Set M⦄, B.Finite → IsAddComplete (A \ B)

theorem IsAddStronglyComplete.isAddComplete {M : Type u_1} [AddCommMonoid M] [Preorder M] {A : Set M} (hA : IsAddStronglyComplete A) : IsAddComplete A

A strongly complete set is complete.

theorem IsAddStronglyComplete.mono {M : Type u_1} [AddCommMonoid M] [Preorder M] {A B : Set M} (h : A ⊆ B) (ha : IsAddStronglyComplete A) : IsAddStronglyComplete B

If A ⊆ B and A is strongly complete, then B is also strongly complete.

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

A sequence A is strongly complete if fun m => A (n + m) is still complete for all n.

Equations

• IsAddStronglyCompleteNatSeq A = ∀ (n : ℕ), IsAddComplete (Set.range fun (m : ℕ) => A (n + m))

theorem IsAddStronglyCompleteNatSeq.isAddComplete {M : Type u_1} [AddCommMonoid M] [Preorder M] {A : ℕ → M} (hA : IsAddStronglyCompleteNatSeq A) : IsAddComplete (Set.range A)

A strongly complete sequence is complete.

theorem IsAddStronglyCompleteNatSeq.of_isAddStronglyComplete {M : Type u_1} [AddCommMonoid M] [Preorder M] {A : ℕ → M} (h : IsAddStronglyComplete (Set.range A)) : IsAddStronglyCompleteNatSeq A

If the range of a sequence A is strongly complete, then A is strongly complete.

theorem IsAddStronglyCompleteNatSeq.isAddStronglyComplete {M : Type u_1} [AddCommMonoid M] [Preorder M] {A : ℕ → M} (h : IsAddStronglyCompleteNatSeq A) (hA : ∀ (m : M), (A ⁻¹' {m}).Finite) : IsAddStronglyComplete (Set.range A)

If A is strongly complete and the preimage of each element is finite, then the range of A is strongly complete.

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