English
Let f: A → B and S be a collection of subsets of A. The image under f of the union of all sets in S equals the union of the images under f of each set in S.
Русский
Пусть f: A → B и S — семейство подмножеств A. Образ под множества каждого элемента S равен объединению образов всех множеств S.
LaTeX
$$$f\left(\bigcup_{A \in S} A\right) = \bigcup_{A \in S} f[A]$$$
Lean4
theorem image_sUnion {f : α → β} {s : Set (Set α)} : (f '' ⋃₀ s) = ⋃₀ (image f '' s) :=
by
ext b
simp only [mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
constructor
· rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
exact ⟨t, ht₁, a, ht₂, rfl⟩
· rintro ⟨t, ht₁, a, ht₂, rfl⟩
exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
