image2_iUnion_right — Mathlib

English

Let f: α × β → γ, and a family (t_i) of subsets of β indexed by i. Then image2 f s (⋃ i, t_i) equals ⋃ i, image2 f s (t_i).

Русский

Пусть f: α × β → γ и семейство подмножеств T_i ⊆ β, индексируемое i. Тогда image2 f s (⋃_i t_i) равно ⋃_i image2 f s (t_i).

LaTeX

$$$$ \\operatorname{image}_2 f s \\left( \\bigcup_i t_i \\right) = \\bigcup_i \\operatorname{image}_2 f s (t_i) $$$$

Lean4

theorem image2_iUnion_right (s : Set α) (t : ι → Set β) : image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i) := by
  simp only [← image_prod, prod_iUnion, image_iUnion]

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