Pointwise operations with lists of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem set.mem_prod_list_of_fn {α : Type u_2} [monoid α] {n : ℕ} {a : α} {s : fin n → set α} :

a ∈ (list.of_fn s).prod ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a

theorem set.mem_sum_list_of_fn {α : Type u_2} [add_monoid α] {n : ℕ} {a : α} {s : fin n → set α} :

a ∈ (list.of_fn s).sum ↔ ∃ (f : Π (i : fin n), ↥(s i)), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a

theorem set.mem_list_sum {α : Type u_2} [add_monoid α] {l : list (set α)} {a : α} :

a ∈ l.sum ↔ ∃ (l' : list (Σ (s : set α), ↥s)), (list.map (λ (x : Σ (s : set α), ↥s), ↑(x.snd)) l').sum = a ∧ list.map sigma.fst l' = l

theorem set.mem_list_prod {α : Type u_2} [monoid α] {l : list (set α)} {a : α} :

a ∈ l.prod ↔ ∃ (l' : list (Σ (s : set α), ↥s)), (list.map (λ (x : Σ (s : set α), ↥s), ↑(x.snd)) l').prod = a ∧ list.map sigma.fst l' = l

theorem set.mem_nsmul {α : Type u_2} [add_monoid α] {s : set α} {a : α} {n : ℕ} :

a ∈ n • s ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).sum = a

theorem set.mem_pow {α : Type u_2} [monoid α] {s : set α} {a : α} {n : ℕ} :

a ∈ s ^ n ↔ ∃ (f : fin n → ↥s), (list.of_fn (λ (i : fin n), ↑(f i))).prod = a