Documentation

Mathlib.Data.Set.Pointwise.BigOperators

Results about pointwise operations on sets and big operators. #

theorem Set.mem_finset_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : Finset ι) (f : ιSet α) (a : α) :
(a Finset.sum t fun i => f i) g x, (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} [inst : AddCommMonoid α] (f : ιSet α) (a : α) (motive : (g h, 0 = a) → Prop) :
(x : g h, 0 = a) → ((w : ια) → (w_1 : ∀ {i : ι}, i w i f i) → (hf : 0 = a) → motive (_ : g h, 0 = a)) → motive x
Equations
theorem Set.mem_finset_prod {α : Type u_2} {ι : Type u_1} [inst : CommMonoid α] (t : Finset ι) (f : ιSet α) (a : α) :
(a Finset.prod t fun i => f i) g x, (Finset.prod t fun i => g i) = a

The n-ary version of Set.mem_mul.

theorem Set.mem_fintype_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] [inst : Fintype ι] (f : ιSet α) (a : α) :
(a Finset.sum Finset.univ fun i => f i) g x, (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_2} {ι : Type u_1} [inst : CommMonoid α] [inst : Fintype ι] (f : ιSet α) (a : α) :
(a Finset.prod Finset.univ fun i => f i) g x, (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_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : List ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg i f i) :

An n-ary version of Set.add_mem_add.

theorem Set.list_prod_mem_list_prod {α : Type u_2} {ι : Type u_1} [inst : CommMonoid α] (t : List ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg i f i) :

An n-ary version of Set.mul_mem_mul.

theorem Set.list_sum_subset_list_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : List ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : ∀ (i : ι), i tf₁ i f₂ i) :

An n-ary version of Set.add_subset_add.

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

An n-ary version of Set.mul_subset_mul.

theorem Set.list_sum_singleton {M : Type u_1} [inst : AddCommMonoid M] (s : List M) :
List.sum (List.map (fun i => {i}) s) = {List.sum s}
theorem Set.list_prod_singleton {M : Type u_1} [inst : CommMonoid M] (s : List M) :
List.prod (List.map (fun i => {i}) s) = {List.prod s}
theorem Set.multiset_sum_mem_multiset_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : Multiset ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg i f i) :

An n-ary version of Set.add_mem_add.

theorem Set.multiset_prod_mem_multiset_prod {α : Type u_2} {ι : Type u_1} [inst : CommMonoid α] (t : Multiset ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg i f i) :

An n-ary version of Set.mul_mem_mul.

theorem Set.multiset_sum_subset_multiset_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : Multiset ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : ∀ (i : ι), i tf₁ i f₂ i) :

An n-ary version of Set.add_subset_add.

theorem Set.multiset_prod_subset_multiset_prod {α : Type u_2} {ι : Type u_1} [inst : CommMonoid α] (t : Multiset ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : ∀ (i : ι), i tf₁ i f₂ i) :

An n-ary version of Set.mul_subset_mul.

theorem Set.multiset_sum_singleton {M : Type u_1} [inst : AddCommMonoid M] (s : Multiset M) :
Multiset.sum (Multiset.map (fun i => {i}) s) = {Multiset.sum s}
theorem Set.multiset_prod_singleton {M : Type u_1} [inst : CommMonoid M] (s : Multiset M) :
Multiset.prod (Multiset.map (fun i => {i}) s) = {Multiset.prod s}
theorem Set.finset_sum_mem_finset_sum {α : Type u_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : Finset ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg 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_2} {ι : Type u_1} [inst : CommMonoid α] (t : Finset ι) (f : ιSet α) (g : ια) (hg : ∀ (i : ι), i tg 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_2} {ι : Type u_1} [inst : AddCommMonoid α] (t : Finset ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : ∀ (i : ι), i tf₁ 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_2} {ι : Type u_1} [inst : CommMonoid α] (t : Finset ι) (f₁ : ιSet α) (f₂ : ιSet α) (hf : ∀ (i : ι), i tf₁ 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_1} {ι : Type u_2} [inst : AddCommMonoid M] (s : Finset ι) (I : ιM) :
(Finset.sum s fun i => {I i}) = {Finset.sum s fun i => I i}
theorem Set.finset_prod_singleton {M : Type u_1} {ι : Type u_2} [inst : CommMonoid M] (s : Finset ι) (I : ιM) :
(Finset.prod s fun i => {I i}) = {Finset.prod s fun i => I i}

TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.