mathlib3documentation

data.set.pointwise.list_of_fn

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 = 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 = 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