mapsTo_iInter₂_iInter₂ — Mathlib

English

If for all i, j, MapsTo f (s_i_j) (t_i_j), then MapsTo f (⋂ i (⋂ j), s_i_j) (⋂ i (⋂ j), t_i_j).

Русский

Если для всех i и j выполняется, что f отображает s_{i,j} в t_{i,j}, тогда f отображает ⋂_{i} ⋂_{j} s_{i,j} в ⋂_{i} ⋂_{j} t_{i,j}.

LaTeX

$$$(\\forall i,j,\\ MapsTo f (s_{i,j}) (t_{i,j})) \\Rightarrow \\ MapsTo f (\\bigcap_i \\bigcap_j s_{i,j}) (\\bigcap_i \\bigcap_j t_{i,j}).$$$

Lean4

theorem mapsTo_iInter₂_iInter₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, MapsTo f (s i j) (t i j)) : MapsTo f (⋂ (i) (j), s i j) (⋂ (i) (j), t i j) :=
  mapsTo_iInter_iInter fun i => mapsTo_iInter_iInter (H i)

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