tendsto_iSup — Mathlib

English

Let f: α → β and x_i: ι → Filter α, y: Filter β. Then Tendsto f (iSup_i x_i) y iff ∀ i, Tendsto f (x_i) y.

Русский

Пусть f: α → β, x_i: ι → Filter α и y: Filter β. Тогда Tendsto f (iSup_i x_i) y эквивалентно ∀ i, Tendsto f (x_i) y.

LaTeX

$$$ \\operatorname{Tendsto} f (\\uplus_i x_i) y \\iff \\forall i, \\operatorname{Tendsto} f (x_i) y $$$

Lean4

@[simp]
theorem tendsto_iSup {f : α → β} {x : ι → Filter α} {y : Filter β} : Tendsto f (⨆ i, x i) y ↔ ∀ i, Tendsto f (x i) y :=
  by simp only [Tendsto, map_iSup, iSup_le_iff]

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