tendsto_atTop_of_monotone_of_filter

English

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

Русский

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

LaTeX

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

Lean4

/-- If a monotone function `u : ι → α` tends to `atTop` along *some* non-trivial filter `l`, then
it tends to `atTop` along `atTop`. -/
theorem tendsto_atTop_of_monotone_of_filter [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u)
    [NeBot l] (hu : Tendsto u l atTop) : Tendsto u atTop atTop :=
  h.tendsto_atTop_atTop fun b => (hu.eventually (mem_atTop b)).exists

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