image2_iInter₂_subset_left — Mathlib

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

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