Documentation

Mathlib.Combinatorics.Additive.SubsetSum

Subset sums #

This file defines the subset sum of a finite subset of a commutative monoid.

References #

source
def Finset.subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] (A : Finset M) :
Finset M

The subset-sum of a finite set A in a commutative monoid is the set of all sums of subsets of A.

Equations
Instances For
    source
    theorem Finset.mem_subsetSum_iff {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} :
    a ∈ A.subsetSum ↔ ∃ B ⊆ A, ∑ b ∈ B, b = a
    source
    @[simp]
    theorem Finset.zero_mem_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :
    0 ∈ A.subsetSum
    source
    @[simp]
    theorem Finset.subsetSum_nonempty {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :
    A.subsetSum.Nonempty
    source
    theorem Finset.subset_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :
    A ⊆ A.subsetSum
    source
    theorem Finset.subsetSum_mono {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A B : Finset M} (hAB : A ⊆ B) :
    A.subsetSum ⊆ B.subsetSum
    source
    @[simp]
    theorem Finset.subsetSum_erase_zero {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :
    (A.erase 0).subsetSum = A.subsetSum
    source
    theorem Finset.vadd_finset_subsetSum_subset_subsetSum_insert {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} (a_notin_A : a ∉ A) :
    a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
    source
    theorem Finset.nonneg_of_mem_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_nonneg : ∀ x ∈ A, 0 ≤ x) (x : M) :
    x ∈ A.subsetSum → 0 ≤ x
    source
    theorem Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (hA : ∀ x ∈ A, 0 < x) (hAa : ∀ x ∈ A, x < a) (ha : 0 < a) :
    A.card + A.subsetSum.card < (insert a A).subsetSum.card
    source
    theorem Finset.card_succ_choose_two_lt_card_subsetSum_of_pos {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_pos : ∀ x ∈ A, 0 < x) :
    (A.card + 1).choose 2 < A.subsetSum.card
    source
    theorem Finset.card_choose_two_lt_card_subsetSum_of_nonneg {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_pos : ∀ x ∈ A, 0 ≤ x) :
    A.card.choose 2 < A.subsetSum.card