surjOn_iUnion — Mathlib

English

If for every i, SurjOn f s (t i), then SurjOn f s (⋃ i t i).

Русский

Если для каждого i выполняется, что f образует s в t_i, тогда f образует s в объединении t_i.

LaTeX

$$$\\forall i,\\ \\text{SurjOn}(f,s,t_i) \\Rightarrow \\text{SurjOn}(f,s,\\bigcup_i t_i).$$$

Lean4

theorem surjOn_iUnion {s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f s (t i)) : SurjOn f s (⋃ i, t i) :=
  surjOn_sUnion <| forall_mem_range.2 H

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