eventually_le_atBot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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