tendsto_piMap_pi — Mathlib

English

If each f i tends from l i to l' i, then Pi.map f tends from pi l to pi l'.

Русский

Если для каждого i функция f i сходится от l i к l' i, то отображение Pi.map сходится от π l к π l'.

LaTeX

$$$\\forall i, Tendsto (f i) (l i) (l' i) \\Rightarrow Tendsto (\\mathrm{Pi.map} f) (\\mathrm{pi}\\, l) (\\mathrm{pi}\\, l')$$$

Lean4

theorem tendsto_piMap_pi {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (α i)} {l' : ∀ i, Filter (β i)}
    (h : ∀ i, Tendsto (f i) (l i) (l' i)) : Tendsto (Pi.map f) (pi l) (pi l') :=
  tendsto_pi.2 fun i ↦ (h i).comp (tendsto_eval_pi _ _)

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