image2_sInter_right_subset — Mathlib

English

The image of the right intersection with a fixed set t is contained in the intersection over S of image2 f t s.

Русский

Образ правой части пересечения с фиксированным множеством t содержится в пересечении по S образа2 f t s.

LaTeX

$$$\\operatorname{image2}(f,t,\\bigcap_0 S) \\subseteq \\bigcap_{s\\in S} \\operatorname{image2}(f,t,s).$$$

Lean4

theorem image2_sInter_right_subset (t : Set α) (S : Set (Set β)) (f : α → β → γ) :
    image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s := by aesop

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