English
Let f be a function from α to subsets of β, and s a subset of α. The union of the image f''s equals the union over a ∈ s of f(a): ⋃₀ (f '' s) = ⋃ a ∈ s, f a.
Русский
Пусть f: α → Set β, и s ⊆ α. Объединение образов f''s равно объединению по всем a ∈ s: ⋃₀ (f '' s) = ⋃ a ∈ s, f a.
LaTeX
$$$$ \\bigcup_{U \\in f''s} U = \\bigcup_{a \\in s} f(a). $$$$
Lean4
@[simp]
theorem sUnion_image (f : α → Set β) (s : Set α) : ⋃₀ (f '' s) = ⋃ a ∈ s, f a :=
sSup_image