tendsto_atBot_isGLB — Mathlib

English

If f is monotone and a is the least upper bound of its range, then f converges to a along atTop.

Русский

Если f монотонна и a является наименьшей верхней гранью диапазона, тогда f сходится к a по atTop.

LaTeX

$$$\\text{Monotone } f \\Rightarrow IsLUB (\\mathrm{range}\, f)\\ a \\Rightarrow \\text{Tendsto } f\\; atTop\\; (nhds\ a).$$$

Lean4

theorem tendsto_atBot_isGLB (h_mono : Monotone f) (ha : IsGLB (Set.range f) a) : Tendsto f atBot (𝓝 a) := by
  convert tendsto_atTop_isLUB h_mono.dual ha.dual using 1

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