image_iUnion — Mathlib

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 (α := α)]

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