range_of_tendsto — Mathlib

English

If every f i is bounded below by a and f tends to a, then a is a greatest lower bound of the range of f.

Русский

Если каждый f i ниже ограничен снизу не менее a и f сходится к a, то a является наибольшей нижней гранью образа функции f.

LaTeX

$$$ (\forall i, a \le f i) \rightarrow Tendsto f F (nhds a) \rightarrow IsGLB (range f) a $$$

Lean4

theorem range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) : IsGLB (range f) a :=
  IsLUB.range_of_tendsto (α := αᵒᵈ) hle hlim

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