image_iInter₂_subset — Mathlib

English

The image of a double intersection is contained in the intersection of the corresponding images.

Русский

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

LaTeX

$$$\\bigcap_{i,j} s_{i,j}$ и равенство в виде $f''(\\bigcap (i)(j) s_{i j}) \\subseteq \\bigcap_{i,j} f'' s_{i j}$.$$

Lean4

theorem image_iInter₂_subset (s : ∀ i, κ i → Set α) (f : α → β) : (f '' ⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), f '' s i j :=
  (mapsTo_iInter₂_iInter₂ fun i hi => mapsTo_image f (s i hi)).image_subset

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