# Results about pointwise operations on sets and big operators. #

theorem Set.image_list_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (l : List (Set α)) :
f '' = List.sum (List.map (fun (s : Set α) => f '' s) l)
abbrev Set.image_list_sum.match_1 {α : Type u_1} (motive : List (Set α)Prop) :
∀ (x : List (Set α)), (Unitmotive [])(∀ (a : Set α) (as : List (Set α)), motive (a :: as))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem Set.image_list_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (l : List (Set α)) :
f '' = List.prod (List.map (fun (s : Set α) => f '' s) l)
theorem Set.image_multiset_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (m : Multiset (Set α)) :
f '' = Multiset.sum (Multiset.map (fun (s : Set α) => f '' s) m)
theorem Set.image_multiset_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (m : Multiset (Set α)) :
f '' = Multiset.prod (Multiset.map (fun (s : Set α) => f '' s) m)
theorem Set.image_finset_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (m : ) (s : ιSet α) :
(f '' Finset.sum m fun (i : ι) => s i) = Finset.sum m fun (i : ι) => f '' s i
theorem Set.image_finset_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [] [] [] (f : F) (m : ) (s : ιSet α) :
(f '' Finset.prod m fun (i : ι) => s i) = Finset.prod m fun (i : ι) => f '' s i
theorem Set.mem_finset_sum {ι : Type u_1} {α : Type u_2} [] (t : ) (f : ιSet α) (a : α) :
(a Finset.sum t fun (i : ι) => f i) ∃ (g : ια) (_ : ∀ {i : ι}, i tg i f i), (Finset.sum t fun (i : ι) => g i) = a

The n-ary version of Set.mem_add.

abbrev Set.mem_finset_sum.match_1 {ι : Type u_1} {α : Type u_2} [] (f : ιSet α) (a : α) (motive : (∃ (g : ια) (_ : ∀ {i : ι}, i g i f i), 0 = a)Prop) :
∀ (x : ∃ (g : ια) (_ : ∀ {i : ι}, i g i f i), 0 = a), (∀ (w : ια) (w_1 : ∀ {i : ι}, i w i f i) (hf : 0 = a), motive (_ : ∃ (g : ια) (_ : ∀ {i : ι}, i g i f i), 0 = a))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem Set.mem_finset_prod {ι : Type u_1} {α : Type u_2} [] (t : ) (f : ιSet α) (a : α) :
(a Finset.prod t fun (i : ι) => f i) ∃ (g : ια) (_ : ∀ {i : ι}, i tg i f i), (Finset.prod t fun (i : ι) => g i) = a

The n-ary version of Set.mem_mul.

theorem Set.mem_fintype_sum {ι : Type u_1} {α : Type u_2} [] [] (f : ιSet α) (a : α) :
(a Finset.sum Finset.univ fun (i : ι) => f i) ∃ (g : ια) (_ : ∀ (i : ι), g i f i), (Finset.sum Finset.univ fun (i : ι) => g i) = a

A version of Set.mem_finset_sum with a simpler RHS for sums over a Fintype.

theorem Set.mem_fintype_prod {ι : Type u_1} {α : Type u_2} [] [] (f : ιSet α) (a : α) :
(a Finset.prod Finset.univ fun (i : ι) => f i) ∃ (g : ια) (_ : ∀ (i : ι), g i f i), (Finset.prod Finset.univ fun (i : ι) => g i) = a

A version of Set.mem_finset_prod with a simpler RHS for products over a Fintype.

theorem Set.list_sum_mem_list_sum {ι : Type u_1} {α : Type u_2} [] (t : List ι) (f : ιSet α) (g : ια) (hg : it, 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} [] (t : List ι) (f : ιSet α) (g : ια) (hg : it, 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} [] (t : List ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : it, f₁ i f₂ i) :

An n-ary version of Set.add_subset_add.

theorem Set.list_prod_subset_list_prod {ι : Type u_1} {α : Type u_2} [] (t : List ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : it, f₁ i f₂ i) :

An n-ary version of Set.mul_subset_mul.

theorem Set.list_sum_singleton {M : Type u_5} [] (s : List M) :
List.sum (List.map (fun (i : M) => {i}) s) = {}
theorem Set.list_prod_singleton {M : Type u_5} [] (s : List M) :
List.prod (List.map (fun (i : M) => {i}) s) = {}
theorem Set.multiset_sum_mem_multiset_sum {ι : Type u_1} {α : Type u_2} [] (t : ) (f : ιSet α) (g : ια) (hg : it, 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} [] (t : ) (f : ιSet α) (g : ια) (hg : it, g i f i) :

An n-ary version of Set.mul_mem_mul.

theorem Set.multiset_sum_subset_multiset_sum {ι : Type u_1} {α : Type u_2} [] (t : ) (f₁ : ιSet α) (f₂ : ιSet α) (hf : it, f₁ i f₂ i) :

An n-ary version of Set.add_subset_add.

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

An n-ary version of Set.mul_subset_mul.

theorem Set.multiset_sum_singleton {M : Type u_5} [] (s : ) :
Multiset.sum (Multiset.map (fun (i : M) => {i}) s) = {}
theorem Set.multiset_prod_singleton {M : Type u_5} [] (s : ) :
Multiset.prod (Multiset.map (fun (i : M) => {i}) s) = {}
theorem Set.finset_sum_mem_finset_sum {ι : Type u_1} {α : Type u_2} [] (t : ) (f : ιSet α) (g : ια) (hg : it, g i f i) :
(Finset.sum t fun (i : ι) => g i) Finset.sum t fun (i : ι) => f i

An n-ary version of Set.add_mem_add.

theorem Set.finset_prod_mem_finset_prod {ι : Type u_1} {α : Type u_2} [] (t : ) (f : ιSet α) (g : ια) (hg : it, g i f i) :
(Finset.prod t fun (i : ι) => g i) Finset.prod t fun (i : ι) => f i

An n-ary version of Set.mul_mem_mul.

theorem Set.finset_sum_subset_finset_sum {ι : Type u_1} {α : Type u_2} [] (t : ) (f₁ : ιSet α) (f₂ : ιSet α) (hf : it, f₁ i f₂ i) :
(Finset.sum t fun (i : ι) => f₁ i) Finset.sum t fun (i : ι) => f₂ i

An n-ary version of Set.add_subset_add.

theorem Set.finset_prod_subset_finset_prod {ι : Type u_1} {α : Type u_2} [] (t : ) (f₁ : ιSet α) (f₂ : ιSet α) (hf : it, f₁ i f₂ i) :
(Finset.prod t fun (i : ι) => f₁ i) Finset.prod t fun (i : ι) => f₂ i

An n-ary version of Set.mul_subset_mul.

theorem Set.finset_sum_singleton {M : Type u_5} {ι : Type u_6} [] (s : ) (I : ιM) :
(Finset.sum s fun (i : ι) => {I i}) = {Finset.sum s fun (i : ι) => I i}
theorem Set.finset_prod_singleton {M : Type u_5} {ι : Type u_6} [] (s : ) (I : ιM) :
(Finset.prod s fun (i : ι) => {I i}) = {Finset.prod s fun (i : ι) => I i}
theorem Set.image_finset_sum_pi {ι : Type u_1} {α : Type u_2} [] (l : ) (S : ιSet α) :
(fun (f : ια) => Finset.sum l fun (i : ι) => f i) '' Set.pi (l) S = Finset.sum l fun (i : ι) => S i

The n-ary version of Set.add_image_prod.

theorem Set.image_finset_prod_pi {ι : Type u_1} {α : Type u_2} [] (l : ) (S : ιSet α) :
(fun (f : ια) => Finset.prod l fun (i : ι) => f i) '' Set.pi (l) S = Finset.prod l fun (i : ι) => S i

The n-ary version of Set.image_mul_prod.

theorem Set.image_fintype_sum_pi {ι : Type u_1} {α : Type u_2} [] [] (S : ιSet α) :
(fun (f : ια) => Finset.sum Finset.univ fun (i : ι) => f i) '' Set.pi Set.univ S = Finset.sum Finset.univ fun (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} [] [] (S : ιSet α) :
(fun (f : ια) => Finset.prod Finset.univ fun (i : ι) => f i) '' Set.pi Set.univ S = Finset.prod Finset.univ fun (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.