Results about pointwise operations on sets and big operators.

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

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

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

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

theorem Set.image_finsetProd {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [CommMonoid α] [CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α) : ⇑f '' ∏ i ∈ m, s i = ∏ i ∈ m, ⇑f '' s i

theorem Set.image_finsetSum {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α) : ⇑f '' ∑ i ∈ m, s i = ∑ i ∈ m, ⇑f '' s i

@[deprecated Set.image_finsetSum (since := "2026-04-08")]

theorem Set.image_finset_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α) : ⇑f '' ∑ i ∈ m, s i = ∑ i ∈ m, ⇑f '' s i

Alias of Set.image_finsetSum.

@[deprecated Set.image_finsetProd (since := "2026-04-08")]

theorem Set.image_finset_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [CommMonoid α] [CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α) : ⇑f '' ∏ i ∈ m, s i = ∏ i ∈ m, ⇑f '' s i

Alias of Set.image_finsetProd.

theorem Set.mem_finsetProd {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α) : a ∈ ∏ i ∈ t, f i ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a

The n-ary version of Set.mem_mul.

theorem Set.mem_finsetSum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α) : a ∈ ∑ i ∈ t, f i ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∑ i ∈ t, g i = a

The n-ary version of Set.mem_add.

@[deprecated Set.mem_finsetSum (since := "2026-04-08")]

theorem Set.mem_finset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α) : a ∈ ∑ i ∈ t, f i ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∑ i ∈ t, g i = a

Alias of Set.mem_finsetSum.

---

The n-ary version of Set.mem_add.

@[deprecated Set.mem_finsetProd (since := "2026-04-08")]

theorem Set.mem_finset_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α) : a ∈ ∏ i ∈ t, f i ↔ ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a

Alias of Set.mem_finsetProd.

---

The n-ary version of Set.mem_mul.

theorem Set.mem_pow_iff_prod {α : Type u_2} [CommMonoid α] {n : ℕ} {s : Set α} {a : α} : a ∈ s ^ n ↔ ∃ (f : Fin n → α), (∀ (i : Fin n), f i ∈ s) ∧ ∏ i : Fin n, f i = a

theorem Set.mem_nsmul_iff_sum {α : Type u_2} [AddCommMonoid α] {n : ℕ} {s : Set α} {a : α} : a ∈ n • s ↔ ∃ (f : Fin n → α), (∀ (i : Fin n), f i ∈ s) ∧ ∑ i : Fin n, f i = a

theorem Set.mem_fintype_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] [Fintype ι] (f : ι → Set α) (a : α) : a ∈ ∏ i : ι, f i ↔ ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a

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

theorem Set.mem_fintype_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Fintype ι] (f : ι → Set α) (a : α) : a ∈ ∑ i : ι, f i ↔ ∃ (g : ι → α) (_ : ∀ (i : ι), g i ∈ f i), ∑ i : ι, g i = a

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

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

An n-ary version of Set.mul_mem_mul.

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

An n-ary version of Set.add_mem_add.

theorem Set.list_prod_subset_list_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ 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_subset_list_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ 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_singleton {M : Type u_5} [Monoid M] (s : List M) : (List.map (fun (i : M) => {i}) s).prod = {s.prod}

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

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

An n-ary version of Set.mul_mem_mul.

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

An n-ary version of Set.add_mem_add.

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

An n-ary version of Set.mul_subset_mul.

theorem Set.multiset_sum_subset_multiset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α) (hf : ∀ 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_prod_singleton {M : Type u_5} [CommMonoid M] (s : Multiset M) : (Multiset.map (fun (i : M) => {i}) s).prod = {s.prod}

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

theorem Set.finsetProd_mem_finsetProd {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : ∏ i ∈ t, g i ∈ ∏ i ∈ t, f i

An n-ary version of Set.mul_mem_mul.

theorem Set.finsetSum_mem_finsetSum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : ∑ i ∈ t, g i ∈ ∑ i ∈ t, f i

An n-ary version of Set.add_mem_add.

@[deprecated Set.finsetSum_mem_finsetSum (since := "2026-04-08")]

theorem Set.finset_sum_mem_finset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : ∑ i ∈ t, g i ∈ ∑ i ∈ t, f i

Alias of Set.finsetSum_mem_finsetSum.

---

An n-ary version of Set.add_mem_add.

@[deprecated Set.finsetProd_mem_finsetProd (since := "2026-04-08")]

theorem Set.finset_prod_mem_finset_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : ∏ i ∈ t, g i ∈ ∏ i ∈ t, f i

Alias of Set.finsetProd_mem_finsetProd.

---

An n-ary version of Set.mul_mem_mul.

theorem Set.finsetProd_subset_finsetProd {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i

An n-ary version of Set.mul_subset_mul.

theorem Set.finsetSum_subset_finsetSum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, f₂ i

An n-ary version of Set.add_subset_add.

@[deprecated Set.finsetSum_subset_finsetSum (since := "2026-04-08")]

theorem Set.finset_sum_subset_finset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, f₂ i

Alias of Set.finsetSum_subset_finsetSum.

---

An n-ary version of Set.add_subset_add.

@[deprecated Set.finsetProd_subset_finsetProd (since := "2026-04-08")]

theorem Set.finset_prod_subset_finset_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i

Alias of Set.finsetProd_subset_finsetProd.

---

An n-ary version of Set.mul_subset_mul.

theorem Set.finsetProd_singleton {M : Type u_5} {ι : Type u_6} [CommMonoid M] (s : Finset ι) (I : ι → M) : ∏ i ∈ s, {I i} = {∏ i ∈ s, I i}

theorem Set.finsetSum_singleton {M : Type u_5} {ι : Type u_6} [AddCommMonoid M] (s : Finset ι) (I : ι → M) : ∑ i ∈ s, {I i} = {∑ i ∈ s, I i}

@[deprecated Set.finsetSum_singleton (since := "2026-04-08")]

theorem Set.finset_sum_singleton {M : Type u_5} {ι : Type u_6} [AddCommMonoid M] (s : Finset ι) (I : ι → M) : ∑ i ∈ s, {I i} = {∑ i ∈ s, I i}

Alias of Set.finsetSum_singleton.

@[deprecated Set.finsetProd_singleton (since := "2026-04-08")]

theorem Set.finset_prod_singleton {M : Type u_5} {ι : Type u_6} [CommMonoid M] (s : Finset ι) (I : ι → M) : ∏ i ∈ s, {I i} = {∏ i ∈ s, I i}

Alias of Set.finsetProd_singleton.

theorem Set.image_finsetProd_pi {ι : Type u_1} {α : Type u_2} [CommMonoid α] (l : Finset ι) (S : ι → Set α) : (fun (f : ι → α) => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i

The n-ary version of Set.image_mul_prod.

theorem Set.image_finsetSum_pi {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (l : Finset ι) (S : ι → Set α) : (fun (f : ι → α) => ∑ i ∈ l, f i) '' (↑l).pi S = ∑ i ∈ l, S i

The n-ary version of Set.add_image_prod.

@[deprecated Set.image_finsetSum_pi (since := "2026-04-08")]

theorem Set.image_finset_sum_pi {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (l : Finset ι) (S : ι → Set α) : (fun (f : ι → α) => ∑ i ∈ l, f i) '' (↑l).pi S = ∑ i ∈ l, S i

Alias of Set.image_finsetSum_pi.

---

The n-ary version of Set.add_image_prod.

@[deprecated Set.image_finsetProd_pi (since := "2026-04-08")]

theorem Set.image_finset_prod_pi {ι : Type u_1} {α : Type u_2} [CommMonoid α] (l : Finset ι) (S : ι → Set α) : (fun (f : ι → α) => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i

Alias of Set.image_finsetProd_pi.

---

The n-ary version of Set.image_mul_prod.

theorem Set.image_fintype_prod_pi {ι : Type u_1} {α : Type u_2} [CommMonoid α] [Fintype ι] (S : ι → Set α) : (fun (f : ι → α) => ∏ i : ι, f i) '' univ.pi S = ∏ i : ι, S i

A special case of Set.image_finsetProd_pi for Finset.univ.

theorem Set.image_fintype_sum_pi {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Fintype ι] (S : ι → Set α) : (fun (f : ι → α) => ∑ i : ι, f i) '' univ.pi S = ∑ i : ι, S i

A special case of Set.image_finsetSum_pi for Finset.univ.

TODO: define decidable_mem_finsetProd and decidable_mem_finsetSum.