prod_left — Mathlib

English

The product version of Little-o decomposes into Little-o bounds for each component.

Русский

Производная лямбда-малость распадается на малость по каждому компоненту.

LaTeX

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

Lean4

theorem prod_left (hf : f' =o[l] k') (hg : g' =o[l] k') : (fun x => (f' x, g' x)) =o[l] k' :=
  IsLittleO.of_isBigOWith fun _c hc => (hf.forall_isBigOWith hc).prod_left_same (hg.forall_isBigOWith hc)

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