English
Let f: α → β → γ, s : ∀ i, κ i → Set α, t ⊆ β. Then image2 f (⋂ (i) (j), s i j) t ⊆ ⋂ (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 (\\bigcap_{i} \\bigcap_{j} s_{i,j}) t \\subseteq \\bigcap_{i} \\bigcap_{j} \\operatorname{image}_2 f (s_{i,j}) t $$$$
Lean4
theorem image2_sInter_subset_right (s : Set α) (T : Set (Set β)) : image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t :=
by
rw [sInter_eq_biInter]
exact image2_iInter₂_subset_right ..