English
For a function f and a list of sets l, the image of the product of the sets equals the product of the images: f''(prod l) = prod (f'' s) over s ∈ l.
Русский
Для функции f и списка множеств l образ произведения множеств равен произведению образов: f''(prod l) = prod (f'' s).
LaTeX
$$f''(l.prod) = (l.map (fun s => f'' s)).prod$$
Lean4
@[to_additive]
theorem image_list_prod (f : F) : ∀ l : List (Set α), (f : α → β) '' l.prod = (l.map fun s => f '' s).prod
| [] => image_one.trans <| congr_arg singleton (map_one f)
| a :: as => by rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]