Results about pointwise operations on sets and big operators. #
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_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_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 α)
:
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 α)
:
theorem
Set.mem_finset_sum
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
(t : Finset ι)
(f : ι → Set α)
(a : α)
:
The n-ary version of Set.mem_add.
theorem
Set.mem_finset_prod
{ι : Type u_1}
{α : Type u_2}
[CommMonoid α]
(t : Finset ι)
(f : ι → Set α)
(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 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 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 ∈ 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}
[CommMonoid α]
(t : List ι)
(f : ι → Set α)
(g : ι → α)
(hg : ∀ 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}
[AddCommMonoid α]
(t : List ι)
(f₁ : ι → Set α)
(f₂ : ι → Set α)
(hf : ∀ i ∈ t, 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}
[CommMonoid α]
(t : List ι)
(f₁ : ι → Set α)
(f₂ : ι → Set α)
(hf : ∀ i ∈ t, f₁ i ⊆ f₂ i)
:
An n-ary version of Set.mul_subset_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_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_subset_multiset_sum
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
(t : Multiset ι)
(f₁ : ι → Set α)
(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_subset_multiset_prod
{ι : Type u_1}
{α : Type u_2}
[CommMonoid α]
(t : Multiset ι)
(f₁ : ι → Set α)
(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_singleton
{M : Type u_5}
[AddCommMonoid M]
(s : Multiset M)
:
(Multiset.map (fun (i : M) => {i}) s).sum = {s.sum}
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.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
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 ∈ t, g i ∈ f i)
:
∏ i ∈ t, g i ∈ ∏ i ∈ t, 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 ∈ t, f₁ i ⊆ f₂ i)
:
∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, 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 ∈ t, f₁ i ⊆ f₂ i)
:
∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, 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)
:
∑ i ∈ s, {I i} = {∑ i ∈ s, I i}
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}
theorem
Set.image_finset_sum_pi
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
(l : Finset ι)
(S : ι → Set α)
:
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 α)
:
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 α)
:
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 α)
:
A special case of Set.image_finset_prod_pi for Finset.univ.
TODO: define decidable_mem_finset_prod and decidable_mem_finset_sum.