English
Let s(i,j) ⊆ α and t(i,j) ⊆ β for all i and j (where j ranges over κ(i)). If f maps each s(i,j) into t(i,j), then f maps the union over all i and j of s(i,j) into the union over all i and j of t(i,j).
Русский
Пусть s(i,j) ⊆ α и t(i,j) ⊆ β для всех i и j (где j пробегает по κ(i)). Если отображение f переводит каждое s(i,j) в t(i,j), то оно переводит объединение всех s(i,j) в объединение всех t(i,j).
LaTeX
$$$\\left( \\forall i \\forall j,\\ f[ s(i,j) ] \\subseteq t(i,j) \\right) \\Rightarrow f\\left[ \\bigcup_i \\bigcup_j s(i,j) \\right] \\subseteq \\bigcup_i \\bigcup_j t(i,j).$$$
Lean4
theorem mapsTo_iUnion₂_iUnion₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
(H : ∀ i j, MapsTo f (s i j) (t i j)) : MapsTo f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j) :=
mapsTo_iUnion_iUnion fun i => mapsTo_iUnion_iUnion (H i)
