English
Let f: α × β → γ, s_i_j ⊆ α for all i,j. Then image2 f (⋂ i (j), s_i_j) t ⊆ ⋂ i (j), image2 f (s_i_j) t.
Русский
Пусть f: α × β → γ, s_{i,j} ⊆ α. Тогда image2 f (⋂_{i,j} s_{i,j}) t ⊆ ⋂_{i,j} image2 f (s_{i,j}) t.
LaTeX
$$$$ \\operatorname{image}_2 f \\left( \\bigcap_{i,j} s_{i,j} \\right) t \\subseteq \\bigcap_{i,j} \\operatorname{image}_2 f (s_{i,j}) t $$$$
Lean4
theorem image2_iInter₂_subset_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_subset_iff, mem_iInter]
exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy