isBigO_fst_prod'

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

For f' : α → E' × F' (product space), the first projection is Big-O of f' with respect to l: (fst f') =O_l f'.

Русский

Для f' : α → E' × F' в произведенном пространстве первая проекция есть O_l f'.

LaTeX

$$$(\\text{fst } f') =O_l f'$$$

Lean4

theorem isBigO_fst_prod' {f' : α → E' × F'} : (fun x => (f' x).1) =O[l] f' := by
  simpa [IsBigO_def, IsBigOWith_def] using isBigO_fst_prod (E' := E') (F' := F')

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

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

Разделы

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

Аффилиация

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