image2_iUnion_left — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\operatorname{image}_2 f \\left( \\bigcup_i s_i \\right) t = \\bigcup_i \\operatorname{image}_2 f (s_i) t $$$$

Lean4

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

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