tendsto_iInf_iInf — Mathlib

English

If for every i, Tendsto f (x_i) (y_i), then Tendsto f (iInf_i x_i) (iInf_i y_i).

Русский

Если для каждого i выполняется Tendsto f (x_i) (y_i), то Tendsto f (iInf_i x_i) (iInf_i y_i).

LaTeX

$$$ \\left( \\forall i, \\operatorname{Tendsto} f (x_i) (y_i) \\right) \\Rightarrow \\operatorname{Tendsto} f (\\inf_i x_i) (\\inf_i y_i) $$$

Lean4

theorem tendsto_iInf_iInf {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ i, Tendsto f (x i) (y i)) :
    Tendsto f (iInf x) (iInf y) :=
  tendsto_iInf.2 fun i => tendsto_iInf' i (h i)

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