sUnion_image — Mathlib

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

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