eventually_ge_atTop — Mathlib

English

If f tends to infinity along atTop, then for every 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{Eventual}(c \le f x)\ l.$$$$

Lean4

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

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