image2_iInter₂_subset_right — Mathlib

English

Let f: α × β → γ, s_i_j ⊆ α, 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 \\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_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_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

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