isBigO_snd_prod

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigO_snd_prod

English

Let α be a type, E', F' normed, and l a filter. Then g' =O_l (x ↦ (f'(x), g'(x))) holds if and only if g' =O_l f'.

Русский

Пусть α — тип; f' : α → E'; g' : α → F'; l — фильтр. Тогда g' =O_l (x ↦ (f'(x), g'(x))) эквивалентно g' = O_l f'.

LaTeX

$$$g' =O_l\\ (\\lambda x.(f'(x), g'(x))) \\iff g' =O_l f'$$$

Lean4

theorem isBigO_snd_prod : g' =O[l] fun x => (f' x, g' x) :=
  isBigOWith_snd_prod.isBigO

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

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

Разделы

Аффилиация

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