eventually_gt_atTop — Mathlib

English

If f tends to infinity along a filter atTop, then for every real c, eventually f(x) > c.

Русский

Если f стремится к бесконечности вдоль фильтра atTop, то для любого числа c существует область перехода, после которой f(x) > c.

LaTeX

$$$$\text{If } hf : \operatorname{Tendsto} f\ l\ atTop, \text{ then } \forall c, \operatorname{Eventually}(c < f x)\ l.$$$$

Lean4

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

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