tendsto_iSup_iSup — Mathlib

English

If ∀ i, Tendsto f (x_i) (y_i), then Tendsto f (iSup_i x_i) (iSup_i y_i).

Русский

Если для всех i имеет место Tendsto f (x_i) (y_i), тогда Tendsto f (iSup_i x_i) (iSup_i y_i).

LaTeX

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

Lean4

theorem tendsto_iSup_iSup {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ i, Tendsto f (x i) (y i)) :
    Tendsto f (iSup x) (iSup y) :=
  tendsto_iSup.2 fun i => (h i).mono_right <| le_iSup _ _

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