image2_sInter_subset_right — Mathlib

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 ..

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