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)
:
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_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.multiset_sum_mem_multiset_sum
{α : Type u_2}
{ι : Type u_1}
[inst : 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_2}
{ι : Type u_1}
[inst : 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_2}
{ι : Type u_1}
[inst : 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_2}
{ι : Type u_1}
[inst : 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_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 ∈ 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_2}
{ι : Type u_1}
[inst : 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_2}
{ι : Type u_1}
[inst : 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_2}
{ι : Type u_1}
[inst : 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_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
.