prod_left_snd — Mathlib

English

Additional equivalent formulations expressing that the product bound is equivalent to the conjunction of component bounds for Big-O.

Русский

Дополнительные эквивалентные формулировки, показывающие эквивалентность произведенного ограничения и сочетания ограничений компонентов.

LaTeX

$$IsBigOWith prod_left_isBigOWith_iff$$

Lean4

theorem prod_left_snd : (fun x => (f' x, g' x)) =O[l] k' → g' =O[l] k' :=
  IsBigO.trans isBigO_snd_prod

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