image2_iUnion₂_right — Mathlib

English

Let f: α × β → γ, s ⊆ α, t : ∀ i, κ i → Set β. Then image2 f s (⋃ (i) (j), t i j) equals ⋃ (i) (j), image2 f s (t i j).

Русский

Пусть f: α × β → γ, s ⊆ α, t_{i,j} ⊆ β. Тогда image2 f s ⋃_{i,j} t_{i,j} = ⋃_{i,j} image2 f s t_{i,j}.

LaTeX

$$$$ \\operatorname{image}_2 f s (\\bigcup_{i,j} t_{i,j}) = \\bigcup_{i,j} \\operatorname{image}_2 f s (t_{i,j}) $$$$

Lean4

theorem image2_iUnion₂_right (s : Set α) (t : ∀ i, κ i → Set β) :
    image2 f s (⋃ (i) (j), t i j) = ⋃ (i) (j), image2 f s (t i j) := by simp_rw [image2_iUnion_right]

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