prod_left_fst

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.prod_left_fst

English

Equivalences showing that product Little-O is equivalent to the conjunction of Little-O for each component.

Русский

Эквивалентность: произведение маленькой O эквивалентно конъюнкции по каждому компоненту.

LaTeX

$$IsLittleO_prod_left_eq$$

Lean4

theorem prod_left_fst : (fun x => (f' x, g' x)) =o[l] k' → f' =o[l] k' :=
  IsBigO.trans_isLittleO isBigO_fst_prod

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

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

Разделы

Аффилиация

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