Results about pointwise operations on sets and big operators.

theorem Set.image_list_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddMonoid α] [AddMonoid β] [AddMonoidHomClass F α β] (f : F) (l : List (Set α)) : ↑f '' List.sum l = List.sum (List.map (fun s => ↑f '' s) l)

abbrev Set.image_list_sum.match_1 {α : Type u_1} (motive : List (Set α) → Prop) : (x : List (Set α)) → (Unit → motive []) → ((a : Set α) → (as : List (Set α)) → motive (a :: as)) → motive x

Equations

• Set.image_list_sum.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail

theorem Set.image_list_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [Monoid α] [Monoid β] [MonoidHomClass F α β] (f : F) (l : List (Set α)) : ↑f '' List.prod l = List.prod (List.map (fun s => ↑f '' s) l)

theorem Set.image_multiset_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Multiset (Set α)) : ↑f '' Multiset.sum m = Multiset.sum (Multiset.map (fun s => ↑f '' s) m)

theorem Set.image_multiset_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [CommMonoid α] [CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Multiset (Set α)) : ↑f '' Multiset.prod m = Multiset.prod (Multiset.map (fun s => ↑f '' s) m)

theorem Set.image_finset_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Finset ι) (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} [CommMonoid α] [CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Finset ι) (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} [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} [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

• Set.mem_finset_sum.match_1 f a motive x h_1 = Exists.casesOn x fun w h => Exists.casesOn h fun w_1 h => h_1 w w_1 h

theorem Set.mem_finset_prod {ι : Type u_1} {α : Type u_2} [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_1} {α : Type u_2} [AddCommMonoid α] [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_1} {α : Type u_2} [CommMonoid α] [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_1} {α : Type u_2} [AddCommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) : List.sum (List.map g t) ∈ List.sum (List.map f t)

An n-ary version of Set.add_mem_add.

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

An n-ary version of Set.mul_mem_mul.

theorem Set.list_sum_subset_list_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : List ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) : List.sum (List.map f₁ t) ⊆ List.sum (List.map f₂ t)

An n-ary version of Set.add_subset_add.

theorem Set.list_prod_subset_list_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : List ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) : List.prod (List.map f₁ t) ⊆ List.prod (List.map f₂ t)

An n-ary version of Set.mul_subset_mul.

theorem Set.list_sum_singleton {M : Type u_5} [AddCommMonoid M] (s : List M) : List.sum (List.map (fun i => {i}) s) = {List.sum s}

theorem Set.list_prod_singleton {M : Type u_5} [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_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → g i ∈ f i) : Multiset.sum (Multiset.map g t) ∈ Multiset.sum (Multiset.map f t)

An n-ary version of Set.add_mem_add.

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

An n-ary version of Set.mul_mem_mul.

theorem Set.multiset_sum_subset_multiset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) : Multiset.sum (Multiset.map f₁ t) ⊆ Multiset.sum (Multiset.map f₂ t)

An n-ary version of Set.add_subset_add.

theorem Set.multiset_prod_subset_multiset_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Multiset ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) : Multiset.prod (Multiset.map f₁ t) ⊆ Multiset.prod (Multiset.map f₂ t)

An n-ary version of Set.mul_subset_mul.

theorem Set.multiset_sum_singleton {M : Type u_5} [AddCommMonoid M] (s : Multiset M) : Multiset.sum (Multiset.map (fun i => {i}) s) = {Multiset.sum s}

theorem Set.multiset_prod_singleton {M : Type u_5} [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_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → 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} [CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ (i : ι), i ∈ t → 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} [AddCommMonoid α] (t : Finset ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → 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} [CommMonoid α] (t : Finset ι) (f₁ : ι → Set α) (f₂ : ι → Set α) (hf : ∀ (i : ι), i ∈ t → 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} [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_5} {ι : Type u_6} [CommMonoid M] (s : Finset ι) (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} [AddCommMonoid α] (l : Finset ι) (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} [CommMonoid α] (l : Finset ι) (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} [AddCommMonoid α] [Fintype ι] (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} [CommMonoid α] [Fintype ι] (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.