Documentation

Mathlib.Data.Set.Pointwise.ListOfFn

Pointwise operations with lists of sets #

This file proves some lemmas about pointwise algebraic operations with lists of sets.

theorem Set.mem_sum_list_ofFn {α : Type u_1} [AddMonoid α] {n : } {a : α} {s : Fin nSet α} :
a (List.ofFn s).sum ∃ (f : (i : Fin n) → (s i)), (List.ofFn fun (i : Fin n) => (f i)).sum = a
theorem Set.mem_prod_list_ofFn {α : Type u_1} [Monoid α] {n : } {a : α} {s : Fin nSet α} :
a (List.ofFn s).prod ∃ (f : (i : Fin n) → (s i)), (List.ofFn fun (i : Fin n) => (f i)).prod = a
theorem Set.mem_list_sum {α : Type u_1} [AddMonoid α] {l : List (Set α)} {a : α} :
a l.sum ∃ (l' : List ((s : Set α) × s)), (List.map (fun (x : (s : Set α) × s) => x.snd) l').sum = a List.map Sigma.fst l' = l
theorem Set.mem_list_prod {α : Type u_1} [Monoid α] {l : List (Set α)} {a : α} :
a l.prod ∃ (l' : List ((s : Set α) × s)), (List.map (fun (x : (s : Set α) × s) => x.snd) l').prod = a List.map Sigma.fst l' = l
theorem Set.mem_nsmul {α : Type u_1} [AddMonoid α] {s : Set α} {a : α} {n : } :
a n s ∃ (f : Fin ns), (List.ofFn fun (i : Fin n) => (f i)).sum = a
theorem Set.mem_pow {α : Type u_1} [Monoid α] {s : Set α} {a : α} {n : } :
a s ^ n ∃ (f : Fin ns), (List.ofFn fun (i : Fin n) => (f i)).prod = a