tendsto_atTop_atTop_of_monotone — Mathlib

English

If f is monotone and cofinal (for every b there exists a with b ≤ f(a)), then f tends to atTop along atTop.

Русский

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

LaTeX

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

Lean4

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

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