tendsto_atBot_atBot_of_monotone — Mathlib

English

If f is monotone and for every b there exists a with f(a) ≤ b, then f tends to atBot when its input tends to atBot.

Русский

Если f монотонна и для каждого b существует a с f(a) ≤ b, тогда f стремится к -∞ по направлению atBot.

LaTeX

$$$\operatorname{Tendsto} f\; \operatorname{atBot} \operatorname{atBot}$$$

Lean4

theorem tendsto_atBot_atBot_of_monotone [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f)
    (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atBot atBot :=
  tendsto_iInf.2 fun b =>
    tendsto_principal.2 <|
      let ⟨a, ha⟩ := h b;
      mem_of_superset (mem_atBot a) fun _a' ha' => le_trans (hf ha') ha

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