tendsto_atTop_of_monotone_of_subseq

English

If a monotone function u has a subsequence φ with Tendsto(u ∘ φ) to atTop, then Tendsto u atTop atTop.

Русский

Если монотонная функция u имеет subsequence φ, для которой u ∘ φ стремится к +∞, то u стремится к +∞ по atTop.

LaTeX

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

Lean4

theorem tendsto_atTop_of_monotone_of_subseq [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι} (h : Monotone u)
    {l : Filter ι'} [NeBot l] (H : Tendsto (u ∘ φ) l atTop) : Tendsto u atTop atTop :=
  tendsto_atTop_of_monotone_of_filter h (tendsto_map' H)

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