tendsto_atTop_nhds — Mathlib

English

For a function f: α→X with α ordered and OrderTop, Tendsto f atTop to nhds (f ⊤).

Русский

Для функции f: α→X при упорядочении α и наличии OrderTop, предел при atTop достигает nhds(f(top)).

LaTeX

$$$\\text{Tendsto } f\\ atTop\\ (\\mathcal{N}(f\\top)).$$$

Lean4

theorem tendsto_atTop_nhds [PartialOrder α] [OrderTop α] (f : α → X) : Tendsto f atTop (𝓝 (f ⊤)) :=
  (tendsto_atTop_pure f).mono_right (pure_le_nhds _)

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