tendsto_atTop_ciInf — Mathlib

English

Let f be an antitone function ι → α with a bounded below range in a ConditionallyCompleteLattice. Then f tends to the infimum of its values when i tends to the top.

Русский

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

LaTeX

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

Lean4

theorem tendsto_atTop_ciInf (h_anti : Antitone f) (hbdd : BddBelow <| range f) : Tendsto f atTop (𝓝 (⨅ i, f i)) := by
  convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1

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