tendsto_atBot_of_monotone_of_filter

English

If a monotone function u tends to atBot along a subsequence φ, then u tends to atBot along atBot.

Русский

Если монотонная функция u стремится к -∞ по subsequence, то и по atBot.

LaTeX

$$$\operatorname{Tendsto} u \operatorname{atBot} \operatorname{atBot}$$$

Lean4

/-- If a monotone function `u : ι → α` tends to `atBot` along *some* non-trivial filter `l`, then
it tends to `atBot` along `atBot`. -/
theorem tendsto_atBot_of_monotone_of_filter [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u)
    [NeBot l] (hu : Tendsto u l atBot) : Tendsto u atBot atBot :=
  @tendsto_atTop_of_monotone_of_filter ιᵒᵈ αᵒᵈ _ _ _ _ h.dual _ hu

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