surjOn_iInter — Mathlib

English

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

Русский

Если для каждого i выполняется SurjOn f s (t i), то SurjOn f s (⋃ i t i).

LaTeX

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

Lean4

theorem surjOn_iInter [Nonempty ι] {s : ι → Set α} {t : Set β} {f : α → β} (H : ∀ i, SurjOn f (s i) t)
    (Hinj : InjOn f (⋃ i, s i)) : SurjOn f (⋂ i, s i) t :=
  by
  intro y hy
  rw [Hinj.image_iInter_eq, mem_iInter]
  exact fun i => H i hy

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