tendsto_atTop_atBot — Mathlib

English

Dual to the above, Tendsto f atTop atBot iff for every b there exists i with f(a) ≤ b for all a ≥ i.

Русский

Двойственно предыдущему: Tendsto f atTop atBot эквивалентно существованию i, такого что для всех a ≥ i выполняется f(a) ≤ b.

LaTeX

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

Lean4

theorem tendsto_atTop_atBot : Tendsto f atTop atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → f a ≤ b :=
  tendsto_atTop_atTop (β := βᵒᵈ)

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