surjOn_iUnion₂ — Mathlib

English

For a two-parameter family s i j and t i j, if for all i,j SurjOn f (s i j) (t i j), then SurjOn f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j).

Русский

Для парного семейства s_{i j} и t_{i j}, если для всех i,j выполняется SurjOn f(s_{i j}, t_{i j}), то En surjOn f на двойном объединении.

LaTeX

$$$\\forall i,j,\\ \\text{SurjOn}(f, s_{i j}, t_{i j}) \\Rightarrow \\text{SurjOn}(f, \\bigcup_i\\bigcup_j s_{i j}, \\bigcup_i\\bigcup_j t_{i j}).$$$

Lean4

theorem surjOn_iUnion₂ {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} (H : ∀ i j, SurjOn f s (t i j)) :
    SurjOn f s (⋃ (i) (j), t i j) :=
  surjOn_iUnion fun i => surjOn_iUnion (H i)

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