surjOn_iUnion_iUnion — Mathlib

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 _)

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