eventually_lt_atBot — Mathlib

English

If f tends to bottom along atBot, then for every c, eventually f(x) < c.

Русский

Если функция стремится к нижней границе вдоль atBot, то для любого c в конечном счёте f(x) < c.

LaTeX

$$$$\text{If } hf : \operatorname{Tendsto} f\ l\ atBot, \; \forall c, \operatorname{Eventual}(f x < c)\ l.$$$$

Lean4

protected theorem eventually_lt_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot)
    (c : β) : ∀ᶠ x in l, f x < c :=
  hf.eventually (eventually_lt_atBot c)

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