Set.finset_prod_mem_finset_prod
theorem Set.finset_prod_mem_finset_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (t.prod fun i => g i) ∈ t.prod fun i => f i
The theorem `Set.finset_prod_mem_finset_prod` states that for any type `ι`, and a commutative monoid `α`, given a finite set `t` of type `ι`, a function `f` mapping elements of `ι` to sets of `α`, and a function `g` mapping elements of `ι` to `α`, if every element `i` of `t` satisfies the property that `g(i)` is an element of `f(i)`, then the product (under the operation of the commutative monoid) of `g` evaluated at each element in `t` is an element of the product of sets `f` evaluated at each element in `t`. In mathematical terms, if $\forall i \in t, g(i) \in f(i)$, then $\prod_{i \in t} g(i) \in \prod_{i \in t} f(i)$.
More concisely: If `f : ι → Set α` is a function and `g : ι → α` is such that `g i ∈ f i` for all `i ∈ finset ι t`, then `∏ i in t, g i ∈ ∏ i in t, f i`.
|
Set.multiset_sum_mem_multiset_sum
theorem Set.multiset_sum_mem_multiset_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (Multiset.map g t).sum ∈ (Multiset.map f t).sum
The theorem `Set.multiset_sum_mem_multiset_sum` states that for any type `ι` and any commutative monoid `α`, given a multiset `t` of type `ι`, a function `f` mapping `ι` to a set of `α`, and a function `g` mapping `ι` to `α`, if every element `i` in the multiset `t` satisfies that `g i` is in the set `f i`, then the sum of the multiset obtained by mapping `g` over `t` is in the sum of the multiset obtained by mapping `f` over `t`.
In simpler words, if each element in our multiset, when passed through function `g`, results in a value that belongs to the set produced by the same element passed through function `f`, then the sum of the transformed multiset using function `g` belongs to the sum of the transformed multiset using function `f`.
More concisely: If `g(i) ∈ ⋃ i : ι. f i` for all `i : ι` in a multiset `t`, then `∑ i : ι. g i ∈ ∑ i : ι. f i`.
|
Set.finset_sum_mem_finset_sum
theorem Set.finset_sum_mem_finset_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (t.sum fun i => g i) ∈ t.sum fun i => f i
The theorem `Set.finset_sum_mem_finset_sum` states that for any type `ι` and any commutative monoid `α`, given a finite set `t` of type `ι`, a function `f` mapping elements of `ι` to sets of `α`, and a function `g` mapping elements of `ι` to `α`, if each element `g i` is in the set `f i` for all `i` in `t`, then the sum of the elements `g i` (as calculated by the `sum` function acting on `t` and `g`) is in the set resulting from the sum of the sets `f i` (as calculated by the `sum` function acting on `t` and `f`).
More concisely: For any commutative monoid `α`, if `t` is a finite set, `f : ι → set α`, and `g : ι → α` are such that `g i ∈ f i` for all `i` in `t`, then `∑ i in t, g i ∈ ∑ i in t, f i`.
|
Set.mem_fintype_prod
theorem Set.mem_fintype_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Fintype ι] (f : ι → Set α) (a : α),
(a ∈ Finset.univ.prod fun i => f i) ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), (Finset.univ.prod fun i => g i) = a
This theorem, `Set.mem_fintype_prod`, states that for any types `ι` and `α` (where `α` has a commutative monoid structure and `ι` is a finite type), given a function `f` from `ι` to the set of `α` and an element `a` of `α`, `a` is in the product over the finite set `Finset.univ` using the function `f` if and only if there exists another function `g` such that for all `i` in `ι`, `g(i)` is in `f(i)`, and the product of `g(i)` over `Finset.univ` equals `a`.
In more simple terms, it says that an element is a product of some set function if and only if it can be produced by another function that maps each index to an element in the corresponding set, and the product of these mapped elements equals the original element.
More concisely: For a finite type `ι` and a commutative monoid `α`, an element `a` lies in the product of `α` indexed by `ι` via a function `f` if and only if there exists a function `g` such that `a` is the product of `g(i)` in `f(i)` for all `i` in `ι`.
|
Set.image_finset_prod_pi
theorem Set.image_finset_prod_pi :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (l : Finset ι) (S : ι → Set α),
(fun f => l.prod fun i => f i) '' (↑l).pi S = l.prod fun i => S i
The theorem `Set.image_finset_prod_pi` states that for any given finite set `l` of an arbitrary type `ι`, and a function `S` that maps every element of `ι` to a set of elements of some commutative monoid `α`, the image of the product function `(l.prod fun i => f i)` over the cartesian product `(↑l).pi S` (which is the set of all functions from `l` to the union of set `S` for every element in `l`) is equal to the product of the set `S` for every element in `l`. In simpler terms, this theorem is about the relationship between the image of a product function and a cartesian product in the context of sets and finite sets.
More concisely: For any finite set `l` and a function `S : ι -> Set algebraic _`, the image of `l.prod f` over `(↑l).pi S` equals the product of the sets in `S` indexed by elements of `l`.
|
Set.image_fintype_prod_pi
theorem Set.image_fintype_prod_pi :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Fintype ι] (S : ι → Set α),
(fun f => Finset.univ.prod fun i => f i) '' Set.univ.pi S = Finset.univ.prod fun i => S i
The theorem `Set.image_fintype_prod_pi` states that for any type `ι`, a type `α` which is a commutative monoid, and a function `S` from `ι` to the set of `α`, the image under the function that maps a function `f` to the product over the universe of `ι` of `f i`, of the set of all functions from the universe of `ι` to the respective sets `S i`, is equal to the product over the universe of `ι` of the sets `S i`. This theorem is a special case of `Set.image_finset_prod_pi` applied to the universal finite set `Finset.univ`.
More concisely: For any commutative monoid type `α` and function `S : ι → α`, the image of the function that maps a function `f` to the product of `f i` over `ι` of the set of all functions from `ι` to `S i`, is equal to the product over `ι` of the sets `S i`.
|
Set.mem_finset_prod
theorem Set.mem_finset_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
(a ∈ t.prod fun i => f i) ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), (t.prod fun i => g i) = a
This theorem, named `Set.mem_finset_prod`, states that for any type `ι` and any commutative monoid `α`, given a finite set `t` of type `ι`, a function `f` mapping from `ι` to sets of `α`, and an element `a` of `α`, `a` is in the product of the sets `f i` for `i` in `t` if and only if there exists a function `g` such that for all `i` in `t`, `g i` is in `f i`, and the product of `g i` for `i` in `t` equals `a`. This is the n-ary version of `Set.mem_mul`, describing the membership condition for the product of a collection of sets indexed by a finite set.
More concisely: For any finite set $T$, type $\ι$, commutative monoid $\alpha$, function $f$ from $\ι$ to subsets of $\alpha$, and element $a$ in $\alpha$, $a$ is in the product of sets $f(i)$ for $i$ in $T$ if and only if there exists a function $g$ such that $g(i)$ is in $f(i)$ for all $i$ in $T$ and $\prod\_{i \in T} g(i) = a$.
|
Set.image_finset_sum_pi
theorem Set.image_finset_sum_pi :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (l : Finset ι) (S : ι → Set α),
(fun f => l.sum fun i => f i) '' (↑l).pi S = l.sum fun i => S i
This theorem, named `Set.image_finset_sum_pi`, states that for any given type `ι`, another type `α` which has an additive commutative monoid structure, a finite set `l` of type `ι`, and a function `S` that maps elements of `ι` to sets of `α`, the image of the function `(fun f => l.sum fun i => f i)` on the set of functions defined on `l` with values in the respective sets `S i` is the same as the sum over all elements `i` in `l` of the set `S i`. In simpler terms, it asserts that the sum of the images of the elements of `l` under the function `f` is equal to the sum of the sets `S i` for each element `i` in `l`.
More concisely: For any type `ι`, set `l` of finite size from `ι`, function `S : ι → set α`, and function `f : l → α`, the sum of images `∑ i in l, f i` equals the set sum `∑ i in l, S i`.
|
Set.list_sum_subset_list_sum
theorem Set.list_sum_subset_list_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (List.map f₁ t).sum ⊆ (List.map f₂ t).sum
This theorem states that given an additive commutative monoid `α`, a list `t` of type `ι`, and two mappings `f₁` and `f₂` from `ι` to the set of `α`, if for every element `i` in the list `t`, the set `f₁ i` is a subset of the set `f₂ i`, then the sum of the list obtained by mapping `f₁` over the list `t` is a subset of the sum of the list obtained by mapping `f₂` over the list `t`. Essentially, it asserts that if every individual element of a list maps to a subset under one function compared to another, then the sum of those subsets under the first function is itself a subset of the sum under the second function.
More concisely: Given an additive commutative monoid `α`, if for every `i` in a list `t`, `f₁ i ⊆ f₂ i`, then `∑i in t, f₁ i ⊆ ∑i in t, f₂ i`.
|
Set.list_sum_mem_list_sum
theorem Set.list_sum_mem_list_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (List.map g t).sum ∈ (List.map f t).sum
The theorem `Set.list_sum_mem_list_sum` states that for any type `ι` and any type `α` that forms an additive commutative monoid, given a list `t` of elements of type `ι`, a function `f` from `ι` to sets of `α`, and a function `g` from `ι` to `α`, if every element `i` in the list `t` maps via `g` into the corresponding set `f(i)`, then the sum of the list obtained by applying `g` to each element in `t` is an element of the sum of the list obtained by applying `f` to each element in `t`. The sum here is the standard sum in the additive commutative monoid `α`.
More concisely: For any additive commutative monoid type `α` and lists `t` of index type `ι`, functions `f : ι → sets α` and `g : ι → α`, if for all `i ∈ t`, `g i ∈ f i`, then `∑ i in t, g i ∈ ∑ i in t, f i`.
|
Set.list_prod_subset_list_prod
theorem Set.list_prod_subset_list_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (List.map f₁ t).prod ⊆ (List.map f₂ t).prod
This theorem, `Set.list_prod_subset_list_prod`, is a generalization of the concept of `Set.mul_subset_mul` for an n-ary operation. It states that for any type `ι`, any commutative monoid `α` and any list `t` of `ι`, if you have two functions, `f₁` and `f₂`, mapping `ι` to a set of `α` such that for every element `i` in the list `t`, the set `f₁ i` is a subset of the set `f₂ i`, then the product of the sets obtained by mapping each element of `t` through `f₁` (denoted `(List.map f₁ t).prod`) is a subset of the product of the sets obtained by mapping each element of `t` through `f₂` (denoted `(List.map f₂ t).prod`). Here, the `.prod` operation corresponds to the product operation of the commutative monoid `α`.
More concisely: For any commutative monoid `α` and list `t` of indices `ι`, if for every index `i` in `t`, `f₁ i ⊆ f₂ i`, then `(List.map f₁ t).prod ⊆ (List.map f₂ t).prod`.
|
Set.list_prod_mem_list_prod
theorem Set.list_prod_mem_list_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (List.map g t).prod ∈ (List.map f t).prod
This theorem states that for any list `t` of elements of some type `ι`, any function `f` mapping `ι` to a set of elements of a commutative monoid `α`, and any function `g` mapping `ι` to `α`, if every element `i` in `t` has the property that `g(i)` is an element of `f(i)`, then the product of the list obtained by mapping `g` over `t` is an element of the product of the list obtained by mapping `f` over `t`. In other words, if each element of a list transformed by `g` is within the corresponding set transformed by `f`, the product of the transformed list by `g` is within the product of the transformed list by `f`.
More concisely: If `f : ι -> set α` is a function mapping each element `i` of a list `t : list ι` to a set containing `g(i) : α` for all `i` in `t`, then `∏(map f t)` contains `∏(map g t)`.
|
Set.image_fintype_sum_pi
theorem Set.image_fintype_sum_pi :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Fintype ι] (S : ι → Set α),
(fun f => Finset.univ.sum fun i => f i) '' Set.univ.pi S = Finset.univ.sum fun i => S i
This theorem states that for any index type `ι`, any type `α` with an additive commutative monoid structure, and any function `S` from `ι` to the set of `α`, the image of the function that maps each function `f` from `ι` to `α` to the sum over the entire `ι` of `f(i)` for each `i` in `ι`, where the domain of definition is the product of sets `S i` for each `i` in the universe, is the same as the sum over the entire `ι` of the sets `S(i)`. In simpler terms, it states that the sum of the elements of the functions in the universal set is the same as the sum of the elements in the universal set itself.
More concisely: For any index type `ι`, any additive commutative monoid `α`, and function `S : ι → α`, the sum of `S i` for all `i` in `ι` equals the sum of the images `Σ i, S i`.
|
Set.mem_finset_sum
theorem Set.mem_finset_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
(a ∈ t.sum fun i => f i) ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), (t.sum fun i => g i) = a
The theorem `Set.mem_finset_sum` states that for any type `ι`, type `α` which is equipped with an addition operation satisfying commutative and associative laws (making it an `AddCommMonoid`), a finite set `t` of elements of type `ι`, a function `f` from `ι` to a set of elements of type `α`, and an element `a` of type `α`, `a` is an element of the summation over `t` of function `f` if and only if there exists a function `g` such that for all elements `i` in `t`, `g i` is in `f i`, and the sum over `t` of `g` equals `a`.
In simpler terms, an element can be represented as the sum of elements from distinct sets (represented by `f`) if there is a function `g` that selects one element from each set such that the sums are equal.
More concisely: For any commutative and associative additive monoid `(ι, +)`, finite set `t ∈ Set ι`, function `f : ι → α`, and `α` element `a`, `a ∈ ∑ i ∈ t (f i)` if and only if there exists a function `g : t → α` such that `∑ i ∈ t g i = a` and `g i ∈ f i` for all `i ∈ t`.
|
Set.multiset_prod_subset_multiset_prod
theorem Set.multiset_prod_subset_multiset_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod
This theorem, `Set.multiset_prod_subset_multiset_prod`, takes as inputs a type `ι`, another type `α` which has a commutative monoid structure, a multiset `t` of type `ι`, and two functions, `f₁` and `f₂`, that map from `ι` to the set of `α`. It states that if for all `i` in the multiset `t`, the set resulting from applying `f₁` to `i` is a subset of the set resulting from applying `f₂` to `i`, then the product over the multiset obtained by mapping `f₁` over `t` is a subset of the product over the multiset obtained by mapping `f₂` over `t`. In other words, if each individual set produced by `f₁` is contained within the corresponding set produced by `f₂`, then the product of all such sets from `f₁` is contained within the product of all such sets from `f₂`.
More concisely: If for each element `i` in a multiset `t`, the image of `i` under function `f₁` is subset of the image of `i` under `f₂`, then the multiset product of `f₁` over `t` is subset of the multiset product of `f₂` over `t`.
|
Set.finset_sum_subset_finset_sum
theorem Set.finset_sum_subset_finset_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (t.sum fun i => f₁ i) ⊆ t.sum fun i => f₂ i
The theorem `Set.finset_sum_subset_finset_sum` states that for any type `ι`, and for any `AddCommMonoid` type `α` with two functions `f₁` and `f₂` from `ι` to the set of `α`, given a finset `t` of `ι`, if for each element `i` in `t`, the set `f₁ i` is a subset of the set `f₂ i`, then the sum over `t` of the sets `f₁ i` is a subset of the sum over `t` of the sets `f₂ i`. In other words, if every individual element's set under `f₁` is a subset of the corresponding set under `f₂`, then the overall union of all such sets under `f₁` is a subset of the union of all such sets under `f₂`.
More concisely: If `f₁ i ⊆ f₂ i` for all `i` in a finset `t`, then `∑ i in t, f₁ i ⊆ ∑ i in t, f₂ i`.
|
Set.multiset_sum_subset_multiset_sum
theorem Set.multiset_sum_subset_multiset_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (Multiset.map f₁ t).sum ⊆ (Multiset.map f₂ t).sum
This theorem, `Set.multiset_sum_subset_multiset_sum`, is a generalized version of the `Set.add_subset_add` theorem. Given a multiset `t` of type `ι`, and two functions `f₁` and `f₂` that map from `ι` to a set of type `α` (where `α` is an additive commutative monoid), if for every element `i` in `t`, the set `f₁ i` is a subset of the set `f₂ i`, then the sum of the multiset obtained by mapping `f₁` over `t` is a subset of the sum of the multiset obtained by mapping `f₂` over `t`. In mathematical terms, the theorem asserts that if $\forall i \in t, f₁(i) \subseteq f₂(i)$, then $\sum_{i \in t} f₁(i) \subseteq \sum_{i \in t} f₂(i)$.
More concisely: If `f₁(i) ⊆ f₂(i)` for all `i` in a multiset `t`, then the sum of the multiset obtained by mapping `f₁` over `t` is a subset of the sum of the multiset obtained by mapping `f₂` over `t`.
|
Set.multiset_prod_mem_multiset_prod
theorem Set.multiset_prod_mem_multiset_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (Multiset.map g t).prod ∈ (Multiset.map f t).prod
This theorem, `Set.multiset_prod_mem_multiset_prod`, is a generalized version of `Set.mul_mem_mul`. It applies to any commutative monoid `α` and states that for any multiset `t` of a type `ι`, and any two functions `f : ι → Set α` and `g : ι → α`, if for all `i` in `t`, `g i` belongs to `f i`, then the product of the elements of the multiset obtained by mapping `g` over `t` belongs to the product of the multisets obtained by mapping `f` over `t`. In other words, it guarantees that the product of the images of a multiset under a certain function belongs to the product of the images of the multisets under another function, given a particular membership condition.
More concisely: If `f : ι --> Set α` and `g : ι --> α` are functions and `t : Set (Set ι)` is a multiset of type `ι` such that `g i ∈ f i` for all `i` in `t`, then `∏ (f i : Set α) (in i : t) = ∏ (g i : Set α) (in i : t)`.
|
Set.finset_prod_subset_finset_prod
theorem Set.finset_prod_subset_finset_prod :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
(∀ i ∈ t, f₁ i ⊆ f₂ i) → (t.prod fun i => f₁ i) ⊆ t.prod fun i => f₂ i
This is a generalized version of the `Set.mul_subset_mul` theorem. The theorem `Set.finset_prod_subset_finset_prod` states that for any type `ι`, any commutative monoid `α`, any finite set `t` of type `ι`, and any two functions `f₁` and `f₂` from `ι` to `Set α`, if for all elements `i` in `t`, the set `f₁ i` is a subset of the set `f₂ i`, then the product of the sets `f₁ i` for all `i` in `t` is a subset of the product of the sets `f₂ i` for all `i` in `t`. The product of a collection of sets is defined in terms of the monoid operation on `α`.
More concisely: If `f₁ i ⊆ f₂ i` for all `i` in a finite set `t`, then `∏i in t, f₁ i ⊆ ∏i in t, f₂ i`.
|
Set.mem_fintype_sum
theorem Set.mem_fintype_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Fintype ι] (f : ι → Set α) (a : α),
(a ∈ Finset.univ.sum fun i => f i) ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), (Finset.univ.sum fun i => g i) = a
This theorem, `Set.mem_fintype_sum`, states that for any types `ι` and `α`, given an additive commutative monoid structure on `α` and a finite type structure on `ι`, for any function `f` from `ι` to a set of elements of type `α`, and for any element `a` of type `α`, `a` is in the sum (over all elements `i` of the finite type `ι`) of the sets `f i` if and only if there exists some function `g` such that for every `i` in `ι`, `g i` is in the set `f i`, and the sum (over all elements `i` of the finite type `ι`) of `g i` equals `a`.
In other words, an element `a` is in the sum of sets indexed by a finite type if and only if it can be represented as the sum of elements from these sets, each chosen by a function.
More concisely: For any finite type `ι` and additive commutative monoid `α`, an element `a` of `α` lies in the sum of the images of a function from `ι` to `α` if and only if it can be expressed as the sum of elements from these images, where each element is chosen by some function from `ι` to the image under the given function.
|