image2_sInter_subset_left — Mathlib

English

Let f: α × β → γ, S a set of subsets of α, and t ⊆ β. Then image2 f (⋂₀ S) t equals ⋃ s ∈ S, image2 f s t.

Русский

Пусть f: α × β → γ, S множество подмножеств α, и t ⊆ β. Тогда image2 f (⋂₀ S) t = ⋃_{s∈S} image2 f s t.

LaTeX

$$$$ \\operatorname{image}_2 f (\\bigcap_0 S) t = \\bigcup_{s \\in S} \\operatorname{image}_2 f s t $$$$

Lean4

theorem image2_sInter_subset_left (S : Set (Set α)) (t : Set β) : image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t :=
  by
  rw [sInter_eq_biInter]
  exact image2_iInter₂_subset_left ..

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