isBigO_prod_left — Mathlib

English

A simplified form showing that the Big-O for a pair is equivalent to Big-O for each component individually.

Русский

Упрощенная форма: Big-O для пары эквивалентно Big-O для каждого компонента по отдельности.

LaTeX

$$Eq (IsBigO l (fun x => { fst := f' x, snd := g' x }) k') (And (IsBigO l f' k') (IsBigO l g' k'))$$

Lean4

@[simp]
theorem isBigO_prod_left : (fun x => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

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