tendsto_atTop_atTop — Mathlib

English

A function f grows to +∞ along atTop if and only if for every b there is an index i such that for all a with i ≤ a we have b ≤ f(a).

Русский

Функция f растет до бесконечности вдоль atTop тогда и только тогда, когда для каждого b существует индекс i, при котором для всех a ≥ i выполняется b ≤ f(a).

LaTeX

$$$\text{Tendsto } f\ atTop\ atTop \leftrightarrow \forall b, \exists i, \forall a, i \le a \Rightarrow b \le f(a)$$$

Lean4

/-- A function `f` grows to `+∞` independent of an order-preserving embedding `e`. -/
theorem tendsto_atTop_atTop : Tendsto f atTop atTop ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → b ≤ f a :=
  tendsto_iInf.trans <| forall_congr' fun _ => tendsto_atTop_principal

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