tendsto_eval_pi — Mathlib

English

For each index i, the evaluation map at i from the product filter pi f to f i is a Tendsto.

Русский

Для каждого индекса i отображение проекции на i-ую координату из произведения фильтров pi f в f i сохраняет пределы: Tendsto.

LaTeX

$$$\operatorname{Tendsto}(\mathrm{eval}_i)\big(\pi f\big)\big( f_i\big).$$$

Lean4

theorem tendsto_eval_pi (f : ∀ i, Filter (α i)) (i : ι) : Tendsto (eval i) (pi f) (f i) :=
  tendsto_iInf' i tendsto_comap

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