image_list_prod — Mathlib

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 _ _]

Похожие утверждения