tendsto_iInf' — Mathlib

English

If for a family x_i of filters on α we have Tendsto f (x_i) y for some i, then Tendsto f (iInf_j x_j) y.

Русский

Если для семейства фильтров x_i на α имеем Tendsto f (x_i) y для некоторого i, то Tendsto f (iInf_j x_j) y.

LaTeX

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

Lean4

theorem tendsto_iInf' {f : α → β} {x : ι → Filter α} {y : Filter β} (i : ι) (hi : Tendsto f (x i) y) :
    Tendsto f (⨅ i, x i) y :=
  hi.mono_left <| iInf_le _ _

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