surjOn_iUnion₂_iUnion₂ — Mathlib

English

Same as above: a two-parameter union surjectivity principle.

Русский

То же самое: принцип сюръективности на объединении с двумя индексами.

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₂_iUnion₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, SurjOn f (s i j) (t i j)) : SurjOn f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j) :=
  surjOn_iUnion_iUnion fun i => surjOn_iUnion_iUnion (H i)

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