tendsto_atBot_ciInf — Mathlib

English

Let f be a monotone function from a directed set ι into a ConditionallyCompleteLattice α, whose range is bounded below. Then f tends to the infimum of its values, that is, f(i) converges to inf_i f(i) along the bottom filter.

Русский

Пусть f: ι → α — монотонная функция, где ι — ориентированное множество, α — условно полноупорядоченная решетка, образ f ограничен снизу. Тогда f стремится кInf f(i) по нижнему фильтру

LaTeX

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

Lean4

theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) : Tendsto f atBot (𝓝 (⨅ i, f i)) := by
  convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1

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