English
If for each i, SurjOn f (s i) (t i) holds, then SurjOn f (⋃ i s i) (⋃ i t i).
Русский
Если для каждого i выполняется, что f отображает s_i в t_i, то f отображает объединение s_i в объединение t_i.
LaTeX
$$$\\forall i,\\ \\text{SurjOn}(f, s_i, t_i) \\Rightarrow \\text{SurjOn}(f, \\bigcup_i s_i, \\bigcup_i t_i).$$$
Lean4
theorem surjOn_iUnion_iUnion {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f (s i) (t i)) :
SurjOn f (⋃ i, s i) (⋃ i, t i) :=
surjOn_iUnion fun i => (H i).mono (subset_iUnion _ _) (Subset.refl _)