iUnion_image_right — Mathlib

English

Let f: α × β → γ be a function and s ⊆ α, t ⊆ β. Then the union over b ∈ t of the image of s under a ↦ f(a,b) equals the set of all values f(a,b) with a ∈ s and b ∈ t.

Русский

Пусть f: α × β → γ — функция, и S ⊆ α, T ⊆ β. Тогда объединение по b ∈ T изображений множества S через отображение a ↦ f(a,b) равно множеству всех значений f(a,b) при a ∈ S и b ∈ T.

LaTeX

$$$$ \\bigcup_{b \\in t} \\{ f(a,b) \\mid a \\in s \\} = \\{ f(a,b) \\mid a \\in s, b \\in t \\} $$$$

Lean4

theorem iUnion_image_right : ⋃ b ∈ t, (f · b) '' s = image2 f s t := by rw [image2_swap, iUnion_image_left]

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