Documentation

Mathlib.Data.Set.Pointwise.BigOperators

Results about pointwise operations on sets and big operators. #

theorem Set.image_list_sum {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [AddMonoid α] [AddMonoid β] [AddMonoidHomClass F α β] (f : F) (l : List (Set α)) :
f '' l.sum = (List.map (fun (s : Set α) => f '' s) l).sum
abbrev Set.image_list_sum.match_1 {α : Type u_1} (motive : List (Set α)Prop) :
∀ (x : List (Set α)), (Unitmotive [])(∀ (a : Set α) (as : List (Set α)), motive (a :: as))motive x
Equations
  • =
Instances For
    theorem Set.image_list_prod {α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [Monoid α] [Monoid β] [MonoidHomClass F α β] (f : F) (l : List (Set α)) :
    f '' l.prod = (List.map (fun (s : Set α) => f '' s) l).prod
    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 α) :
    f '' im, s i = im, f '' s i
    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 α) :
    f '' im, s i = im, f '' s i
    theorem Set.mem_finset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Finset ι) (f : ιSet α) (a : α) :
    a it, f i ∃ (g : ια) (_ : ∀ {i : ι}, i tg i f i), it, g i = a

    The n-ary version of Set.mem_add.

    abbrev Set.mem_finset_sum.match_1 {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (f : ιSet α) (a : α) (motive : (∃ (g : ια) (_ : ∀ {i : ι}, i g i f i), 0 = a)Prop) :
    ∀ (x : ∃ (g : ια) (_ : ∀ {i : ι}, i g i f i), 0 = a), (∀ (w : ια) (w_1 : ∀ {i : ι}, i w i f i) (hf : 0 = a), motive )motive x
    Equations
    • =
    Instances For
      theorem Set.mem_finset_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] (t : Finset ι) (f : ιSet α) (a : α) :
      a it, f i ∃ (g : ια) (_ : ∀ {i : ι}, i tg i f i), it, g i = 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 i : ι, f i ∃ (g : ια) (_ : ∀ (i : ι), g i f i), 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_1} {α : Type u_2} [CommMonoid α] [Fintype ι] (f : ιSet α) (a : α) :
      a i : ι, f i ∃ (g : ια) (_ : ∀ (i : ι), g i f i), i : ι, g i = 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 : it, g i f i) :
      (List.map g t).sum (List.map f t).sum

      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 : it, g i f i) :
      (List.map g t).prod (List.map f t).prod

      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 : it, f₁ i f₂ i) :
      (List.map f₁ t).sum (List.map f₂ t).sum

      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 : it, f₁ i f₂ i) :
      (List.map f₁ t).prod (List.map f₂ t).prod

      An n-ary version of Set.mul_subset_mul.

      theorem Set.list_sum_singleton {M : Type u_5} [AddCommMonoid M] (s : List M) :
      (List.map (fun (i : M) => {i}) s).sum = {s.sum}
      theorem Set.list_prod_singleton {M : Type u_5} [CommMonoid M] (s : List M) :
      (List.map (fun (i : M) => {i}) s).prod = {s.prod}
      theorem Set.multiset_sum_mem_multiset_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f : ιSet α) (g : ια) (hg : it, 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 : it, 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 : it, 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 : it, 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 : it, g i f i) :
      it, g i it, 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 : it, g i f i) :
      it, g i it, 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 : it, f₁ i f₂ i) :
      it, f₁ i it, 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 : it, f₁ i f₂ i) :
      it, f₁ i it, 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) :
      is, {I i} = {is, I i}
      theorem Set.finset_prod_singleton {M : Type u_5} {ι : Type u_6} [CommMonoid M] (s : Finset ι) (I : ιM) :
      is, {I i} = {is, I i}
      theorem Set.image_finset_sum_pi {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (l : Finset ι) (S : ιSet α) :
      (fun (f : ια) => il, f i) '' (l).pi S = il, S i

      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 α) :
      (fun (f : ια) => il, f i) '' (l).pi S = il, S i

      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 α) :
      (fun (f : ια) => i : ι, f i) '' Set.univ.pi S = 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} [CommMonoid α] [Fintype ι] (S : ιSet α) :
      (fun (f : ια) => i : ι, f i) '' Set.univ.pi S = 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.