tendsto_atBot_atTop — Mathlib

English

Dual to tendsto_atTop_atTop, Tendsto f atBot to atTop iff for all b there exists i with a ≤ i → b ≤ f(a).

Русский

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

LaTeX

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

Lean4

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

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