image_iUnion₂ — Mathlib

English

Let f: α → β and s: ∀ i, κ i → Set α. Then the image of the iterated union equals the iterated union of images: (f '' ⋃ i, ⋃ j, s_i j) = ⋃ i, ⋃ j, f '' s_i j.

Русский

Пусть f: α→β, и для каждого i множество s_i j. Тогда образ двойного объединения равен двойному объединению образов: f''(⋃i ⋃j s_i j) = ⋃i ⋃j f''(s_i j).

LaTeX

$$$\bigl( f''\bigl(\bigcup_{i} \bigcup_{j} s_{i j}\bigr)\bigr) = \bigl(\bigcup_{i} \bigcup_{j} f''(s_{i j})\bigr)$$$

Lean4

theorem image_iUnion₂ (f : α → β) (s : ∀ i, κ i → Set α) : (f '' ⋃ (i) (j), s i j) = ⋃ (i) (j), f '' s i j := by
  simp_rw [image_iUnion]

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