isBigO_one

Mathlib.Analysis.Asymptotics.Lemmas

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

← MathLib Explorer

English

If f =O[l] g and g → y in nhds, then f =O[l] 1 after a normalization by g.

Русский

Если f =O[l] g и g сходится к y, тогда f =O[l] 1 после нормировки на g.

LaTeX

$$trans_tendsto_nhds$$

Lean4

theorem _root_.Filter.Tendsto.isBigO_one {c : E'} (h : Tendsto f' l (𝓝 c)) : f' =O[l] (fun _x => 1 : α → F) :=
  h.norm.isBoundedUnder_le.isBigO_one F

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

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

Разделы

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

Аффилиация

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