prod_left — Mathlib

English

If f =O_l g and g =O_l h with bounds c and c', then the combined bound is max(c, c') on the pair (f, g).

Русский

Если f =O_l g и g =O_l h при константах c и c', то для пары (f, g) действует максимум констант.

LaTeX

$$hf : IsBigOWith c l f' k' → hg : IsBigOWith c' l g' k' → IsBigOWith (max c c') l (λ x, (f' x, g' x)) k'$$

Lean4

theorem prod_left (hf : IsBigOWith c l f' k') (hg : IsBigOWith c' l g' k') :
    IsBigOWith (max c c') l (fun x => (f' x, g' x)) k' :=
  (hf.weaken <| le_max_left c c').prod_left_same (hg.weaken <| le_max_right c c')

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