tendsto_atBot — Mathlib

English

For any f, Tendsto f atBot to atBot holds.

Русский

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

LaTeX

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

Lean4

protected theorem tendsto_atBot : Tendsto f atBot atBot :=
  tendsto_atBot_mono f.map_le_of_map_zero <|
    tendsto_atBot_add_const_left _ _ <|
      (tendsto_atBot_mono fun x => (ceil_lt_add_one x).le) <| tendsto_atBot_add_const_right _ _ tendsto_id

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