mathlib3 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.image_list_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [add_monoid α] [add_monoid β] [add_monoid_hom_class F α β] (f : F) (l : list (set α)) :
f '' l.sum = (list.map (λ (s : set α), f '' s) l).sum
theorem set.image_list_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [monoid α] [monoid β] [monoid_hom_class F α β] (f : F) (l : list (set α)) :
f '' l.prod = (list.map (λ (s : set α), f '' s) l).prod
theorem set.image_multiset_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) (m : multiset (set α)) :
f '' m.sum = (multiset.map (λ (s : set α), f '' s) m).sum
theorem set.image_multiset_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [comm_monoid α] [comm_monoid β] [monoid_hom_class F α β] (f : F) (m : multiset (set α)) :
f '' m.prod = (multiset.map (λ (s : set α), f '' s) m).prod
theorem set.image_finset_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_monoid_hom_class F α β] (f : F) (m : finset ι) (s : ι set α) :
f '' m.sum (λ (i : ι), s i) = m.sum (λ (i : ι), f '' s i)
theorem set.image_finset_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [comm_monoid α] [comm_monoid β] [monoid_hom_class F α β] (f : F) (m : finset ι) (s : ι set α) :
f '' m.prod (λ (i : ι), s i) = m.prod (λ (i : ι), f '' s i)
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)}
theorem set.image_finset_sum_pi {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] (l : finset ι) (S : ι set α) :
(λ (f : ι α), l.sum (λ (i : ι), f i)) '' l.pi S = l.sum (λ (i : ι), S i)

The n-ary version of set.add_image_prod.

theorem set.image_finset_prod_pi {ι : Type u_1} {α : Type u_2} [comm_monoid α] (l : finset ι) (S : ι set α) :
(λ (f : ι α), l.prod (λ (i : ι), f i)) '' l.pi S = l.prod (λ (i : ι), S i)

The n-ary version of set.image_mul_prod.

theorem set.image_fintype_sum_pi {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] [fintype ι] (S : ι set α) :
(λ (f : ι α), finset.univ.sum (λ (i : ι), f i)) '' set.univ.pi S = finset.univ.sum (λ (i : ι), S i)

A special case of set.image_finset_sum_pi for finset.univ.

theorem set.image_fintype_prod_pi {ι : Type u_1} {α : Type u_2} [comm_monoid α] [fintype ι] (S : ι set α) :
(λ (f : ι α), finset.univ.prod (λ (i : ι), f i)) '' set.univ.pi S = finset.univ.prod (λ (i : ι), S i)

A special case of set.image_finset_prod_pi for finset.univ.

TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.