mapsTo_iInter_iInter — Mathlib

English

If for every i, MapsTo f (s_i) (t_i), then MapsTo f (⋂ i, s_i) (⋂ i, t_i).

Русский

Если для каждого i выполнено, что f отображает s_i в t_i, тогда f отображает ⋂_i s_i в ⋂_i t_i.

LaTeX

$$$(\\forall i,\\ MapsTo f (s_i) (t_i)) \\Rightarrow \\ MapsTo f (\\bigcap_i s_i) (\\bigcap_i t_i).$$$

Lean4

theorem mapsTo_iInter_iInter {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, MapsTo f (s i) (t i)) :
    MapsTo f (⋂ i, s i) (⋂ i, t i) :=
  mapsTo_iInter.2 fun i => (H i).mono_left (iInter_subset s i)

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