const_div_atTop

Mathlib.Topology.Algebra.Order.Field

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

English

If g(x) → +∞, then r/g(x) → 0 for any constant r.

Русский

Если g(x) → +∞, то r/g(x) → 0 для любого константного r.

LaTeX

$$If g \xrightarrow{l} +\infty then r/g \xrightarrow{l} 0.$$

Lean4

theorem const_div_atTop (hg : Tendsto g l atTop) (r : 𝕜) : Tendsto (fun n ↦ r / g n) l (𝓝 0) :=
  tendsto_const_nhds.div_atTop hg

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

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

Разделы

Аффилиация

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