trans_tendsto_nhds

Mathlib.Analysis.Asymptotics.Lemmas

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.trans_tendsto_nhds

English

A duplicate form of trans_tendsto_nhds for different namespaces; the same transitivity property.

Русский

Дублированная форма trans_tendsto_nhds для другого пространства; та же транзитивность.

LaTeX

$$trans_tendsto_nhds$$

Lean4

theorem trans_tendsto_nhds (hfg : f =O[l] g') {y : F'} (hg : Tendsto g' l (𝓝 y)) : f =O[l] (fun _x => 1 : α → F) :=
  hfg.trans <| hg.isBigO_one F

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

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

Разделы

Аффилиация

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