tendsto_atBot_iSup — Mathlib

English

Let f be an antitone function ι → α with bounded below range. Then f(i) converges to the supremum sup_i f(i) as i goes to the bottom direction.

Русский

Пусть f: ι → α антимонотонна и образ ограничен снизу; тогда f(i) сходится к supremum f(i) при направлении к нижней границе.

LaTeX

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

Lean4

theorem tendsto_atBot_iSup (h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i)) :=
  tendsto_atBot_ciSup h_anti (OrderTop.bddAbove _)

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