tendsto_atTop_atTop_of_monotone' — Mathlib

English

If u is monotone with linear order codomain and range(u) is unbounded above, then Tendsto u atTop atTop.

Русский

Если u монотонна и кодомонотонная линейная ориентированность, и ее диапазон не ограничен сверху, то Tendsto u atTop atTop.

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
above, then `Tendsto u atTop atTop`. -/
theorem tendsto_atTop_atTop_of_monotone' [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u)
    (H : ¬BddAbove (range u)) : Tendsto u atTop atTop :=
  by
  apply h.tendsto_atTop_atTop
  intro b
  rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
  exact ⟨N, le_of_lt hN⟩

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