mathlib documentation

data.set.pointwise.big_operators

Results about pointwise operations on sets and big operators. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem set.mem_finset_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : finset ι) (f : ι set α) (a : α) :
a t.sum (λ (i : ι), f i) (g : ι α) (hg : {i : ι}, i t g i f i), t.sum (λ (i : ι), g i) = a

The n-ary version of set.mem_add.

theorem set.mem_finset_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : finset ι) (f : ι set α) (a : α) :
a t.prod (λ (i : ι), f i) (g : ι α) (hg : {i : ι}, i t g i f i), t.prod (λ (i : ι), g i) = a

The n-ary version of set.mem_mul.

theorem set.mem_fintype_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] [fintype ι] (f : ι set α) (a : α) :
a finset.univ.prod (λ (i : ι), f i) (g : ι α) (hg : (i : ι), g i f i), finset.univ.prod (λ (i : ι), g i) = a

A version of set.mem_finset_prod with a simpler RHS for products over a fintype.

theorem set.mem_fintype_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] [fintype ι] (f : ι set α) (a : α) :
a finset.univ.sum (λ (i : ι), f i) (g : ι α) (hg : (i : ι), g i f i), finset.univ.sum (λ (i : ι), g i) = a

A version of set.mem_finset_sum with a simpler RHS for sums over a fintype.

theorem set.list_sum_mem_list_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : list ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :

An n-ary version of set.add_mem_add.

theorem set.list_prod_mem_list_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : list ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :

An n-ary version of set.mul_mem_mul.

theorem set.list_sum_subset_list_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : list ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :
(list.map f₁ t).sum (list.map f₂ t).sum

An n-ary version of set.add_subset_add.

theorem set.list_prod_subset_list_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : list ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :
(list.map f₁ t).prod (list.map f₂ t).prod

An n-ary version of set.mul_subset_mul.

theorem set.list_sum_singleton {M : Type u_1} [add_comm_monoid M] (s : list M) :
(list.map (λ (i : M), {i}) s).sum = {s.sum}
theorem set.list_prod_singleton {M : Type u_1} [comm_monoid M] (s : list M) :
(list.map (λ (i : M), {i}) s).prod = {s.prod}
theorem set.multiset_sum_mem_multiset_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : multiset ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :

An n-ary version of set.add_mem_add.

theorem set.multiset_prod_mem_multiset_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : multiset ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :

An n-ary version of set.mul_mem_mul.

theorem set.multiset_prod_subset_multiset_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : multiset ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :

An n-ary version of set.mul_subset_mul.

theorem set.multiset_sum_subset_multiset_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : multiset ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :
(multiset.map f₁ t).sum (multiset.map f₂ t).sum

An n-ary version of set.add_subset_add.

theorem set.multiset_sum_singleton {M : Type u_1} [add_comm_monoid M] (s : multiset M) :
(multiset.map (λ (i : M), {i}) s).sum = {s.sum}
theorem set.multiset_prod_singleton {M : Type u_1} [comm_monoid M] (s : multiset M) :
(multiset.map (λ (i : M), {i}) s).prod = {s.prod}
theorem set.finset_prod_mem_finset_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : finset ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :
t.prod (λ (i : ι), g i) t.prod (λ (i : ι), f i)

An n-ary version of set.mul_mem_mul.

theorem set.finset_sum_mem_finset_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : finset ι) (f : ι set α) (g : ι α) (hg : (i : ι), i t g i f i) :
t.sum (λ (i : ι), g i) t.sum (λ (i : ι), f i)

An n-ary version of set.add_mem_add.

theorem set.finset_prod_subset_finset_prod {α : Type u_1} {ι : Type u_2} [comm_monoid α] (t : finset ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :
t.prod (λ (i : ι), f₁ i) t.prod (λ (i : ι), f₂ i)

An n-ary version of set.mul_subset_mul.

theorem set.finset_sum_subset_finset_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (t : finset ι) (f₁ f₂ : ι set α) (hf : (i : ι), i t f₁ i f₂ i) :
t.sum (λ (i : ι), f₁ i) t.sum (λ (i : ι), f₂ i)

An n-ary version of set.add_subset_add.

theorem set.finset_prod_singleton {M : Type u_1} {ι : Type u_2} [comm_monoid M] (s : finset ι) (I : ι M) :
s.prod (λ (i : ι), {I i}) = {s.prod (λ (i : ι), I i)}
theorem set.finset_sum_singleton {M : Type u_1} {ι : Type u_2} [add_comm_monoid M] (s : finset ι) (I : ι M) :
s.sum (λ (i : ι), {I i}) = {s.sum (λ (i : ι), I i)}

TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.