prod_left — Mathlib

English

Two-sided results: equivalences showing that IsBigO and IsLittleO for pairs can be decomposed into the corresponding statements for each component.

Русский

Двусторонние выводы: разложение IsBigO и IsLittleO для пары на соответствующие утверждения для каждого компонента.

LaTeX

$$hf : IsBigOWith c l (fun x => (f' x, g' x)) k' → hg : IsBigOWith c l f' k' → IsBigOWith c l g' k'$$

Lean4

theorem prod_left (hf : f' =O[l] k') (hg : g' =O[l] k') : (fun x => (f' x, g' x)) =O[l] k' :=
  let ⟨_c, hf⟩ := hf.isBigOWith
  let ⟨_c', hg⟩ := hg.isBigOWith
  (hf.prod_left hg).isBigO

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