div_atTop

Mathlib.Topology.Algebra.Order.Field

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.div_atTop

← MathLib Explorer

English

If f(x) → a and g(x) → +∞, then f(x)/g(x) → 0.

Русский

Если f(x) → a и g(x) → +∞, то f(x)/g(x) → 0.

LaTeX

$$Let f \xrightarrow{l} a and g \xrightarrow{l} +\infty imply f/g \xrightarrow{l} 0.$$

Lean4

theorem div_atTop {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x / g x) l (𝓝 0) :=
  by
  simp only [div_eq_mul_inv]
  exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru