Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Set.image_list_prod theorem

(f : F) : ∀ l : List (Set α), (f : α → β) '' l.prod = (l.map fun s => f '' s).prod

Full source

@[to_additive]
theorem image_list_prod (f : F) :
    ∀ l : List (Set α), (f : α → β) '' l.prod = (l.map fun s => f '' s).prod
  | [] => image_one.trans <| congr_arg singleton (map_one f)
  | a :: as => by rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

Image of Product of Sets under Homomorphism Equals Product of Images for Lists

Informal description

Let $F$ be a type of homomorphisms between monoids $M$ and $N$, and let $f \in F$. For any list $l$ of subsets of $M$, the image of the product of the sets in $l$ under $f$ is equal to the product of the images of the sets in $l$ under $f$. That is, $$ f\left(\prod_{s \in l} s\right) = \prod_{s \in l} f(s). $$

Set.image_multiset_prod theorem

(f : F) : ∀ m : Multiset (Set α), (f : α → β) '' m.prod = (m.map fun s => f '' s).prod

Full source

@[to_additive]
theorem image_multiset_prod (f : F) :
    ∀ m : Multiset (Set α), (f : α → β) '' m.prod = (m.map fun s => f '' s).prod :=
  Quotient.ind <| by
    simpa only [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe] using
      image_list_prod f

Image of Product of Sets under Homomorphism Equals Product of Images for Multisets

Informal description

Let $F$ be a type of homomorphisms between monoids $M$ and $N$, and let $f \in F$. For any multiset $m$ of subsets of $M$, the image of the product of the sets in $m$ under $f$ is equal to the product of the images of the sets in $m$ under $f$. That is, $$ f\left(\prod_{s \in m} s\right) = \prod_{s \in m} f(s). $$

Set.image_finset_prod theorem

(f : F) (m : Finset ι) (s : ι → Set α) : ((f : α → β) '' ∏ i ∈ m, s i) = ∏ i ∈ m, f '' s i

Full source

@[to_additive]
theorem image_finset_prod (f : F) (m : Finset ι) (s : ι → Set α) :
    ((f : α → β) '' ∏ i ∈ m, s i) = ∏ i ∈ m, f '' s i :=
  (image_multiset_prod f _).trans <| congr_arg Multiset.prod <| Multiset.map_map _ _ _

Image of Finite Product of Sets under Homomorphism Equals Product of Images

Informal description

Let $F$ be a type of homomorphisms between monoids $M$ and $N$, and let $f \in F$. For any finite set $m$ indexed by $\iota$ and any family of subsets $(s_i)_{i \in \iota}$ of $M$, the image of the product of the sets $s_i$ under $f$ is equal to the product of the images of the sets $s_i$ under $f$. That is, $$ f\left(\prod_{i \in m} s_i\right) = \prod_{i \in m} f(s_i). $$

Set.mem_finset_prod theorem

 (t : Finset ι) (f : ι → Set α) (a : α) :
  (a ∈ ∏ i ∈ t, f i) ↔ ∃ (g : ι → α) (_ : ∀ {i}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a

Full source

/-- The n-ary version of `Set.mem_mul`. -/
@[to_additive "The n-ary version of `Set.mem_add`."]
theorem mem_finset_prod (t : Finset ι) (f : ι → Set α) (a : α) :
    (a ∈ ∏ i ∈ t, f i) ↔ ∃ (g : ι → α) (_ : ∀ {i}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a := by
  classical
    induction' t using Finset.induction_on with i is hi ih generalizing a
    · simp_rw [Finset.prod_empty, Set.mem_one]
      exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩
    rw [Finset.prod_insert hi, Set.mem_mul]
    simp_rw [Finset.prod_insert hi]
    simp_rw [ih]
    constructor
    · rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
      refine ⟨Function.update g i x, ?_, ?_⟩
      · intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj
      · rw [Finset.prod_update_of_not_mem hi, Function.update_self]
    · rintro ⟨g, hg, rfl⟩
      exact ⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩

Characterization of Elements in Product of Subsets of a Commutative Monoid

Informal description

Let $M$ be a commutative monoid, $\iota$ a finite index set, and $f_i \subseteq M$ a family of subsets indexed by $\iota$. For any element $a \in M$, we have \[ a \in \prod_{i \in \iota} f_i \iff \exists (g : \iota \to M), (\forall i \in \iota, g(i) \in f_i) \text{ and } \prod_{i \in \iota} g(i) = a. \]

Set.mem_pow_iff_prod theorem

{n : ℕ} {s : Set α} {a : α} : a ∈ s ^ n ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ ∏ i, f i = a

Full source

@[to_additive]
lemma mem_pow_iff_prod {n : ℕ} {s : Set α} {a : α} :
    a ∈ s ^ na ∈ s ^ n ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ ∏ i, f i = a := by
  simpa using mem_finset_prod (t := .univ) (f := fun _ : Fin n ↦ s) _

Characterization of Elements in Powers of Subsets of a Commutative Monoid

Informal description

Let $M$ be a commutative monoid, $s \subseteq M$ a subset, and $n$ a natural number. For any element $a \in M$, we have \[ a \in s^n \iff \exists (f : \{0,\dots,n-1\} \to M), (\forall i \in \{0,\dots,n-1\}, f(i) \in s) \text{ and } \prod_{i=0}^{n-1} f(i) = a. \]

Set.mem_fintype_prod theorem

 [Fintype ι] (f : ι → Set α) (a : α) : (a ∈ ∏ i, f i) ↔ ∃ (g : ι → α) (_ : ∀ i, g i ∈ f i), ∏ i, g i = a

Full source

/-- A version of `Set.mem_finset_prod` with a simpler RHS for products over a Fintype. -/
@[to_additive "A version of `Set.mem_finset_sum` with a simpler RHS for sums over a Fintype."]
theorem mem_fintype_prod [Fintype ι] (f : ι → Set α) (a : α) :
    (a ∈ ∏ i, f i) ↔ ∃ (g : ι → α) (_ : ∀ i, g i ∈ f i), ∏ i, g i = a := by
  rw [mem_finset_prod]
  simp

Characterization of Elements in Product of Subsets over a Finite Type

Informal description

Let $M$ be a commutative monoid, $\iota$ a finite type, and $f_i \subseteq M$ a family of subsets indexed by $\iota$. For any element $a \in M$, we have \[ a \in \prod_{i \in \iota} f_i \iff \exists (g : \iota \to M), (\forall i \in \iota, g(i) \in f_i) \text{ and } \prod_{i \in \iota} g(i) = a. \]

Set.list_prod_mem_list_prod theorem

(t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : (t.map g).prod ∈ (t.map f).prod

Full source

/-- An n-ary version of `Set.mul_mem_mul`. -/
@[to_additive "An n-ary version of `Set.add_mem_add`."]
theorem list_prod_mem_list_prod (t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) :
    (t.map g).prod ∈ (t.map f).prod := by
  induction' t with h tl ih
  · simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
  · simp_rw [List.map_cons, List.prod_cons]
    exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

Product of Elements in Subsets Implies Product in Product of Subsets

Informal description

Let $M$ be a monoid, $\iota$ be a type, $t$ be a list of elements of $\iota$, and $f : \iota \to \text{Set } M$ be a function assigning a subset of $M$ to each element of $\iota$. If $g : \iota \to M$ is a function such that for every $i \in t$, $g(i) \in f(i)$, then the product of the elements in the list obtained by applying $g$ to each element of $t$ belongs to the product of the subsets obtained by applying $f$ to each element of $t$. In symbols: if $\forall i \in t, g(i) \in f(i)$, then $\prod_{i \in t} g(i) \in \prod_{i \in t} f(i)$.

Set.list_prod_subset_list_prod theorem

 (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (t.map f₁).prod ⊆ (t.map f₂).prod

Full source

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive "An n-ary version of `Set.add_subset_add`."]
theorem list_prod_subset_list_prod (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) :
    (t.map f₁).prod ⊆ (t.map f₂).prod := by
  induction' t with h tl ih
  · rfl
  · simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Product of Subsets Preserves Subset Relation for Lists

Informal description

Let $M$ be a monoid, $\iota$ be a type, and $t$ be a list of elements of $\iota$. Given two functions $f_1, f_2 : \iota \to \text{Set } M$ such that for every $i \in t$, $f_1(i) \subseteq f_2(i)$, then the product of the subsets $f_1(i)$ for $i \in t$ is contained in the product of the subsets $f_2(i)$ for $i \in t$. In symbols: if $\forall i \in t, f_1(i) \subseteq f_2(i)$, then $\prod_{i \in t} f_1(i) \subseteq \prod_{i \in t} f_2(i)$.

Set.list_prod_singleton theorem

{M : Type*} [Monoid M] (s : List M) : (s.map fun i ↦ ({ i } : Set M)).prod = { s.prod }

Full source

@[to_additive]
theorem list_prod_singleton {M : Type*} [Monoid M] (s : List M) :
    (s.map fun i ↦ ({i} : Set M)).prod = {s.prod} :=
  (map_list_prod (singletonMonoidHom : M →* Set M) _).symm

Product of Singletons Equals Singleton of Product

Informal description

Let $M$ be a monoid and $s$ be a list of elements of $M$. The product of the singleton sets $\{i\}$ for each $i \in s$ is equal to the singleton set containing the product of all elements in $s$. In symbols: $\prod_{i \in s} \{i\} = \{\prod_{i \in s} i\}$.

Set.multiset_prod_mem_multiset_prod theorem

 (t : Multiset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : (t.map g).prod ∈ (t.map f).prod

Full source

/-- An n-ary version of `Set.mul_mem_mul`. -/
@[to_additive "An n-ary version of `Set.add_mem_add`."]
theorem multiset_prod_mem_multiset_prod (t : Multiset ι) (f : ι → Set α) (g : ι → α)
    (hg : ∀ i ∈ t, g i ∈ f i) : (t.map g).prod ∈ (t.map f).prod := by
  induction t using Quotient.inductionOn
  simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]
  exact list_prod_mem_list_prod _ _ _ hg

Product of Elements in Subsets Implies Product in Product of Subsets for Multisets

Informal description

Let $M$ be a commutative monoid, $\iota$ be a type, $t$ be a multiset of elements of $\iota$, and $f : \iota \to \text{Set } M$ be a function assigning a subset of $M$ to each element of $\iota$. If $g : \iota \to M$ is a function such that for every $i \in t$, $g(i) \in f(i)$, then the product of the elements in the multiset obtained by applying $g$ to each element of $t$ belongs to the product of the subsets obtained by applying $f$ to each element of $t$. In symbols: if $\forall i \in t, g(i) \in f(i)$, then $\prod_{i \in t} g(i) \in \prod_{i \in t} f(i)$.

Set.multiset_prod_subset_multiset_prod theorem

 (t : Multiset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (t.map f₁).prod ⊆ (t.map f₂).prod

Full source

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive "An n-ary version of `Set.add_subset_add`."]
theorem multiset_prod_subset_multiset_prod (t : Multiset ι) (f₁ f₂ : ι → Set α)
    (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (t.map f₁).prod ⊆ (t.map f₂).prod := by
  induction t using Quotient.inductionOn
  simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]
  exact list_prod_subset_list_prod _ _ _ hf

Product of Subsets Preserves Subset Relation for Multisets

Informal description

Let $M$ be a commutative monoid, $\iota$ be a type, and $t$ be a multiset of elements of $\iota$. Given two functions $f_1, f_2 : \iota \to \text{Set } M$ such that for every $i \in t$, $f_1(i) \subseteq f_2(i)$, then the product of the subsets $f_1(i)$ for $i \in t$ is contained in the product of the subsets $f_2(i)$ for $i \in t$. In symbols: if $\forall i \in t, f_1(i) \subseteq f_2(i)$, then $\prod_{i \in t} f_1(i) \subseteq \prod_{i \in t} f_2(i)$.

Set.multiset_prod_singleton theorem

{M : Type*} [CommMonoid M] (s : Multiset M) : (s.map fun i ↦ ({ i } : Set M)).prod = { s.prod }

Full source

@[to_additive]
theorem multiset_prod_singleton {M : Type*} [CommMonoid M] (s : Multiset M) :
    (s.map fun i ↦ ({i} : Set M)).prod = {s.prod} :=
  (map_multiset_prod (singletonMonoidHom : M →* Set M) _).symm

Product of Singleton Sets Equals Singleton of Product in Commutative Monoid

Informal description

Let $M$ be a commutative monoid and $s$ be a multiset of elements of $M$. Then the product of the singleton sets $\{i\}$ for each $i \in s$ is equal to the singleton set containing the product of all elements in $s$, i.e., \[ \prod_{i \in s} \{i\} = \left\{ \prod_{i \in s} i \right\}. \]

Set.finset_prod_mem_finset_prod theorem

 (t : Finset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : (∏ i ∈ t, g i) ∈ ∏ i ∈ t, f i

Full source

/-- An n-ary version of `Set.mul_mem_mul`. -/
@[to_additive "An n-ary version of `Set.add_mem_add`."]
theorem finset_prod_mem_finset_prod (t : Finset ι) (f : ι → Set α) (g : ι → α)
    (hg : ∀ i ∈ t, g i ∈ f i) : (∏ i ∈ t, g i) ∈ ∏ i ∈ t, f i :=
  multiset_prod_mem_multiset_prod _ _ _ hg

Product of Elements in Subsets Implies Product in Product of Subsets for Finite Sets

Informal description

Let $M$ be a commutative monoid, $\iota$ be a type, and $t$ be a finite subset of $\iota$. Given a family of subsets $f : \iota \to \text{Set } M$ and a family of elements $g : \iota \to M$ such that for every $i \in t$, $g(i) \in f(i)$, then the product of the elements $\prod_{i \in t} g(i)$ belongs to the product of the subsets $\prod_{i \in t} f(i)$. In symbols: if $\forall i \in t, g(i) \in f(i)$, then $\prod_{i \in t} g(i) \in \prod_{i \in t} f(i)$.

Set.finset_prod_subset_finset_prod theorem

 (t : Finset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i

Full source

/-- An n-ary version of `Set.mul_subset_mul`. -/
@[to_additive "An n-ary version of `Set.add_subset_add`."]
theorem finset_prod_subset_finset_prod (t : Finset ι) (f₁ f₂ : ι → Set α)
    (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : ∏ i ∈ t, f₁ i∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i :=
  multiset_prod_subset_multiset_prod _ _ _ hf

Product of Subsets Preserves Subset Relation for Finite Index Sets

Informal description

Let $M$ be a commutative monoid, $\iota$ be a type, and $t$ be a finite subset of $\iota$. Given two families of subsets $f_1, f_2 : \iota \to \mathcal{P}(M)$ such that for every $i \in t$, $f_1(i) \subseteq f_2(i)$, then the product of the subsets $f_1(i)$ over $i \in t$ is contained in the product of the subsets $f_2(i)$ over $i \in t$. In symbols: if $\forall i \in t, f_1(i) \subseteq f_2(i)$, then $\prod_{i \in t} f_1(i) \subseteq \prod_{i \in t} f_2(i)$.

Set.finset_prod_singleton theorem

{M ι : Type*} [CommMonoid M] (s : Finset ι) (I : ι → M) : ∏ i ∈ s, ({I i} : Set M) = {∏ i ∈ s, I i}

Full source

@[to_additive]
theorem finset_prod_singleton {M ι : Type*} [CommMonoid M] (s : Finset ι) (I : ι → M) :
    ∏ i ∈ s, ({I i} : Set M) = {∏ i ∈ s, I i} :=
  (map_prod (singletonMonoidHom : M →* Set M) _ _).symm

Product of Singletons Equals Singleton of Product in Commutative Monoid

Informal description

Let $M$ be a commutative monoid and $\iota$ be an index type. For any finite set $s \subseteq \iota$ and any family of elements $I : \iota \to M$, the product of singleton sets $\{I(i)\}$ over $i \in s$ equals the singleton set containing the product of elements $\prod_{i \in s} I(i)$. In other words: \[ \prod_{i \in s} \{I(i)\} = \left\{\prod_{i \in s} I(i)\right\}. \]

Set.image_finset_prod_pi theorem

(l : Finset ι) (S : ι → Set α) : (fun f : ι → α => ∏ i ∈ l, f i) '' (l : Set ι).pi S = ∏ i ∈ l, S i

Full source

/-- The n-ary version of `Set.image_mul_prod`. -/
@[to_additive "The n-ary version of `Set.add_image_prod`."]
theorem image_finset_prod_pi (l : Finset ι) (S : ι → Set α) :
    (fun f : ι → α => ∏ i ∈ l, f i) '' (l : Set ι).pi S = ∏ i ∈ l, S i := by
  ext
  simp_rw [mem_finset_prod, mem_image, mem_pi, exists_prop, Finset.mem_coe]

Image of Product Function over Indexed Product Set Equals Product of Sets

Informal description

Let $l$ be a finite set of indices and $S : \iota \to \text{Set } \alpha$ be a family of sets. The image of the product function $\prod_{i \in l} f(i)$ over all functions $f$ in the indexed product set $\prod_{i \in l} S(i)$ is equal to the product of the sets $S(i)$ for $i \in l$, i.e., \[ \left\{ \prod_{i \in l} f(i) \mid f \in \prod_{i \in l} S(i) \right\} = \prod_{i \in l} S(i). \]

Set.image_fintype_prod_pi theorem

[Fintype ι] (S : ι → Set α) : (fun f : ι → α => ∏ i, f i) '' univ.pi S = ∏ i, S i

Full source

/-- A special case of `Set.image_finset_prod_pi` for `Finset.univ`. -/
@[to_additive "A special case of `Set.image_finset_sum_pi` for `Finset.univ`."]
theorem image_fintype_prod_pi [Fintype ι] (S : ι → Set α) :
    (fun f : ι → α => ∏ i, f i) '' univ.pi S = ∏ i, S i := by
  simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S

Image of Product Function over Universal Product Set Equals Product of Sets

Informal description

Let $\iota$ be a finite type and $S : \iota \to \text{Set } \alpha$ be a family of sets. The image of the product function $\prod_{i \in \iota} f(i)$ over all functions $f$ in the universal product set $\prod_{i \in \iota} S(i)$ is equal to the product of the sets $S(i)$ for all $i \in \iota$, i.e., \[ \left\{ \prod_{i \in \iota} f(i) \mid f \in \prod_{i \in \iota} S(i) \right\} = \prod_{i \in \iota} S(i). \]