tendsto_atTop — Mathlib

English

For any f, Tendsto f atTop to atTop holds.

Русский

Для любого f верно Tendsto f atTop to atTop.

LaTeX

$$$\forall f:\CircleDeg1Lift:\; \operatorname{Tendsto}(f, \mathrm{atTop}, \mathrm{atTop})$$$

Lean4

protected theorem tendsto_atTop : Tendsto f atTop atTop :=
  tendsto_atTop_mono f.le_map_of_map_zero <|
    tendsto_atTop_add_const_left _ _ <|
      (tendsto_atTop_mono fun x => (sub_one_lt_floor x).le) <| by
        simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id

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