Pointwise operations with lists of sets

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

theorem Set.mem_prod_list_ofFn {α : Type u_1} [Monoid α] {n : ℕ} {a : α} {s : Fin n → Set α} : a ∈ (List.ofFn s).prod ↔ ∃ (f : (i : Fin n) → ↑(s i)), (List.ofFn fun (i : Fin n) => ↑(f i)).prod = a

theorem Set.mem_sum_list_ofFn {α : Type u_1} [AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Set α} : a ∈ (List.ofFn s).sum ↔ ∃ (f : (i : Fin n) → ↑(s i)), (List.ofFn fun (i : Fin n) => ↑(f i)).sum = a

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_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_pow {α : Type u_1} [Monoid α] {s : Set α} {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ (f : Fin n → ↑s), (List.ofFn fun (i : Fin n) => ↑(f i)).prod = a

theorem Set.mem_nsmul {α : Type u_1} [AddMonoid α] {s : Set α} {a : α} {n : ℕ} : a ∈ n • s ↔ ∃ (f : Fin n → ↑s), (List.ofFn fun (i : Fin n) => ↑(f i)).sum = a