isBigOWith_prod_left — Mathlib

English

IsBigOWith for a product is equivalent to IsBigOWith for both components; i.e., the pair bound holds iff both component bounds hold.

Русский

IsBigOWith пары равносильна и для каждого компонента; пара ограничена тогда и только тогда, когда оба компонента ограничены.

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 isBigOWith_prod_left :
    IsBigOWith c l (fun x => (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ IsBigOWith c l g' k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left_same h.2⟩

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