isBigO_fst_prod

Mathlib.Analysis.Asymptotics.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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