image2_iInter_subset_right — Mathlib

English

Let f: α × β → γ, s ⊆ α, and t_i ⊆ β for i in some index set. Then image2 f s (⋂ i, t_i) is contained in ⋂ i, image2 f s (t_i).

Русский

Пусть f: α × β → γ, s ⊆ α, и t_i ⊆ β. Тогда image2 f s (⋂ i t_i) ⊆ ⋂ i image2 f s (t_i).

LaTeX

$$$$ \\operatorname{image}_2 f s \\left( \\bigcap_i t_i \\right) \\subseteq \\bigcap_i \\operatorname{image}_2 f s (t_i) $$$$

Lean4

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

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