image2_iInter_subset_left — Mathlib

English

For s_i ⊆ α and t ⊆ β, the image2 of the intersection is contained in the intersection of the image2's.

Русский

Пусть f: α × β → γ и семейство подмножеств s_i ⊆ α. Тогда image2 f (⋂ i, s_i) t ⊆ ⋂ i, image2 f (s_i) t.

LaTeX

$$$$ \\operatorname{image}_2 f \\left( \\bigcap_i s_i \\right) t \\subseteq \\bigcap_i \\operatorname{image}_2 f (s_i) t $$$$

Lean4

theorem image2_iInter_subset_left (s : ι → Set α) (t : Set β) : image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t :=
  by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i => mem_image2_of_mem (hx _) hy

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