tendsto_iInf — Mathlib

English

For a family of filters y_i on β and a filter x on α, we have: Tendsto f x (iInf_i y_i) if and only if for every i, Tendsto f x (y_i).

Русский

Пусть y_i — семейство фильтров на β, x — фильтр на α. Тогда: Tendsto f x (iInf_i y_i) эквивалентно ∀ i, Tendsto f x (y_i).

LaTeX

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

Lean4

@[simp]
theorem tendsto_iInf {f : α → β} {x : Filter α} {y : ι → Filter β} : Tendsto f x (⨅ i, y i) ↔ ∀ i, Tendsto f x (y i) :=
  by simp only [Tendsto, le_iInf_iff]

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