English
Let f: α × β → γ, s ⊆ α, t : ∀ i, κ i → Set β. Then image2 f s (⋃ (i) (j), t i j) equals ⋃ (i) (j), image2 f s (t i j).
Русский
Пусть f: α × β → γ, s ⊆ α, t_{i,j} ⊆ β. Тогда image2 f s ⋃_{i,j} t_{i,j} = ⋃_{i,j} image2 f s t_{i,j}.
LaTeX
$$$$ \\operatorname{image}_2 f s (\\bigcup_{i,j} t_{i,j}) = \\bigcup_{i,j} \\operatorname{image}_2 f s (t_{i,j}) $$$$
Lean4
theorem image2_iUnion₂_right (s : Set α) (t : ∀ i, κ i → Set β) :
image2 f s (⋃ (i) (j), t i j) = ⋃ (i) (j), image2 f s (t i j) := by simp_rw [image2_iUnion_right]