tendsto_atBot_atBot_of_monotone' — Mathlib

English

Variant of Tendsto atTop atTop for monotone maps with unbounded range, using a prime form.

Русский

Вариант кривой монотонной функции с несобранным диапазоном, аналогично.

LaTeX

$$$\operatorname{Tendsto} u \operatorname{atTop} \operatorname{atTop}$$$

Lean4

/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
below, then `Tendsto u atBot atBot`. -/
theorem tendsto_atBot_atBot_of_monotone' [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u)
    (H : ¬BddBelow (range u)) : Tendsto u atBot atBot :=
  @tendsto_atTop_atTop_of_monotone' ιᵒᵈ αᵒᵈ _ _ _ h.dual H

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