prod_left_fst — Mathlib

English

In IsBigOWith, the pair bound equals the maximum of the two component bounds; pairing preserves a Big-O bound with the maximum constant.

Русский

В IsBigOWith предел пары равен максимуму констант двух компонентов; пара сохраняет предел Big-O с максимумом констант.

LaTeX

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

Lean4

theorem prod_left_fst (h : IsBigOWith c l (fun x => (f' x, g' x)) k') : IsBigOWith c l f' k' :=
  (isBigOWith_fst_prod.trans h zero_le_one).congr_const <| one_mul c

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