prod_left_same — Mathlib

English

If f' and g' are each O of k' with respect to l and same bound c, then the pair (f', g') is O with the common bound c.

Русский

Если оба f' и g' ограничены одним и тем же пределом, то пара (f', g') имеет одинаковое ограничение.

LaTeX

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

Lean4

theorem prod_left_same (hf : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') :
    IsBigOWith c l (fun x => (f' x, g' x)) k' := by rw [isBigOWith_iff] at *;
  filter_upwards [hf, hg] with x using max_le

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