mapsTo_iUnion_iUnion — Mathlib

English

If for all i, MapsTo f (s i) (t i), then MapsTo f (⋃ i, s i) (⋃ i, t i).

Русский

Если для всех i верно MapsTo f (s i) (t i), то MapsTo f (⋃ i, s i) (⋃ i, t i).

LaTeX

$$$\\big( \\forall i, \\mathrm{MapsTo}\\, f\\,(s_i)\\,(t_i) \\big) \\Rightarrow \\mathrm{MapsTo}\\, f\\, (\\bigcup_i s_i)\\, (\\bigcup_i t_i)$$$

Lean4

theorem mapsTo_iUnion_iUnion {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, MapsTo f (s i) (t i)) :
    MapsTo f (⋃ i, s i) (⋃ i, t i) :=
  mapsTo_iUnion.2 fun i ↦ (H i).mono_right (subset_iUnion t i)

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