image2_sInter_left_subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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