Results about pointwise operations on sets and big operators. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
set.image_list_sum
{α : Type u_2}
{β : Type u_3}
{F : Type u_4}
[add_monoid α]
[add_monoid β]
[add_monoid_hom_class F α β]
(f : F)
(l : list (set α)) :
theorem
set.image_multiset_sum
{α : Type u_2}
{β : Type u_3}
{F : Type u_4}
[add_comm_monoid α]
[add_comm_monoid β]
[add_monoid_hom_class F α β]
(f : F)
(m : multiset (set α)) :
theorem
set.image_multiset_prod
{α : Type u_2}
{β : Type u_3}
{F : Type u_4}
[comm_monoid α]
[comm_monoid β]
[monoid_hom_class F α β]
(f : F)
(m : multiset (set α)) :
theorem
set.image_finset_sum
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{F : Type u_4}
[add_comm_monoid α]
[add_comm_monoid β]
[add_monoid_hom_class 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}
[comm_monoid α]
[comm_monoid β]
[monoid_hom_class F α β]
(f : F)
(m : finset ι)
(s : ι → set α) :
theorem
set.mem_finset_sum
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(a : α) :
The n-ary version of set.mem_add.
theorem
set.mem_finset_prod
{ι : Type u_1}
{α : Type u_2}
[comm_monoid α]
(t : finset ι)
(f : ι → set α)
(a : α) :
The n-ary version of set.mem_mul.
theorem
set.mem_fintype_prod
{ι : Type u_1}
{α : Type u_2}
[comm_monoid α]
[fintype ι]
(f : ι → set α)
(a : α) :
a ∈ finset.univ.prod (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ (i : ι), g i ∈ f i), finset.univ.prod (λ (i : ι), g i) = a
A version of set.mem_finset_prod with a simpler RHS for products over a fintype.
theorem
set.mem_fintype_sum
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
[fintype ι]
(f : ι → set α)
(a : α) :
a ∈ finset.univ.sum (λ (i : ι), f i) ↔ ∃ (g : ι → α) (hg : ∀ (i : ι), g i ∈ f i), finset.univ.sum (λ (i : ι), g i) = a
A version of set.mem_finset_sum with a simpler RHS for sums over a fintype.
theorem
set.list_sum_mem_list_sum
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
(t : list ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), 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}
[comm_monoid α]
(t : list ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), 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}
[add_comm_monoid α]
(t : list ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), 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}
[comm_monoid α]
(t : list ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), 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}
[add_comm_monoid α]
(t : multiset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), 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}
[comm_monoid α]
(t : multiset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), 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_prod_subset_multiset_prod
{ι : Type u_1}
{α : Type u_2}
[comm_monoid α]
(t : multiset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), 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}
[add_comm_monoid α]
(t : multiset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), 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_sum_singleton
{M : Type u_1}
[add_comm_monoid M]
(s : multiset M) :
(multiset.map (λ (i : M), {i}) s).sum = {s.sum}
theorem
set.multiset_prod_singleton
{M : Type u_1}
[comm_monoid M]
(s : multiset M) :
(multiset.map (λ (i : M), {i}) s).prod = {s.prod}
theorem
set.finset_prod_mem_finset_prod
{ι : Type u_1}
{α : Type u_2}
[comm_monoid α]
(t : finset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :
An n-ary version of set.mul_mem_mul.
theorem
set.finset_sum_mem_finset_sum
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
(t : finset ι)
(f : ι → set α)
(g : ι → α)
(hg : ∀ (i : ι), i ∈ t → g i ∈ f i) :
An n-ary version of set.add_mem_add.
theorem
set.finset_prod_subset_finset_prod
{ι : Type u_1}
{α : Type u_2}
[comm_monoid α]
(t : finset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :
An n-ary version of set.mul_subset_mul.
theorem
set.finset_sum_subset_finset_sum
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
(t : finset ι)
(f₁ f₂ : ι → set α)
(hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i) :
An n-ary version of set.add_subset_add.
theorem
set.finset_prod_singleton
{M : Type u_1}
{ι : Type u_2}
[comm_monoid M]
(s : finset ι)
(I : ι → M) :
theorem
set.finset_sum_singleton
{M : Type u_1}
{ι : Type u_2}
[add_comm_monoid M]
(s : finset ι)
(I : ι → M) :
theorem
set.image_finset_sum_pi
{ι : Type u_1}
{α : Type u_2}
[add_comm_monoid α]
(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}
[comm_monoid α]
(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}
[add_comm_monoid α]
[fintype ι]
(S : ι → set α) :
(λ (f : ι → α), finset.univ.sum (λ (i : ι), f i)) '' set.univ.pi S = finset.univ.sum (λ (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}
[comm_monoid α]
[fintype ι]
(S : ι → set α) :
(λ (f : ι → α), finset.univ.prod (λ (i : ι), f i)) '' set.univ.pi S = finset.univ.prod (λ (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.