English
For any function f and any family of subsets s_i, the image of the union equals the union of the images: f''(∪_i s_i) = ∪_i f''(s_i).
Русский
Для произвольной функции f и семейства подмножеств s_i образ объединения равен объединению образов каждого s_i.
LaTeX
$$$f''\left(\bigcup_i s_i\right) = \bigcup_i f''(s_i)$$$
Lean4
theorem image_iUnion {f : α → β} {s : ι → Set α} : (f '' ⋃ i, s i) = ⋃ i, f '' s i :=
by
ext1 x
simp only [mem_image, mem_iUnion, ← exists_and_right, exists_swap (α := α)]