image_sInter_subset — Mathlib

English

The image of the intersection over a family of sets is contained in the intersection of the images.

Русский

Образ пересечения семейства множеств содержится в пересечении образов.

LaTeX

$$$f''\\bigcap_{s\\in S} s \\subseteq \\bigcap_{s\\in S} f''s$$$

Lean4

theorem image_sInter_subset (S : Set (Set α)) (f : α → β) : f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s :=
  by
  rw [sInter_eq_biInter]
  apply image_iInter₂_subset

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