image2_iUnion₂_left — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\operatorname{image}_2 f \\left( \\bigcup_{i,j} s_{i,j} \\right) t = \\bigcup_{i} \\bigcup_{j} \\operatorname{image}_2 f (s_{i,j}) t $$$$

Lean4

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

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