tendsto_atTop_iSup — Mathlib

English

If f is monotone, the net f(i) converges to the supremum i↦f(i) under the right completeness assumptions (i.e., iSup).

Русский

Если f монотонна, то f(i) сходится к супремуму функции i ↦ f(i) при заданном полноте и топологическом условии.

LaTeX

$$$ \operatorname{Tendsto} f \operatorname{atTop} \left( \nhds\left( \sup_{i} f(i) \right)\right)$$$

Lean4

theorem tendsto_atTop_iSup (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) :=
  tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _)

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