tendsto_atTop_pure — Mathlib

English

For any function f, Tendsto f atTop to the pure image of f(⊤).

Русский

Для любой функции f выполнено, что Tendsto f при вершине переходит в чистый образ f(⊤).

LaTeX

$$$$ \operatorname{Tendsto} f\ \text{atTop} \ \text{toPure}(f\top). $$$$

Lean4

theorem tendsto_atTop_pure [PartialOrder α] [OrderTop α] (f : α → β) : Tendsto f atTop (pure <| f ⊤) :=
  (OrderTop.atTop_eq α).symm ▸ tendsto_pure_pure _ _

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