trans — Mathlib

English

If f =OWith c l f g and g =OWith c' l g k, then f =OWith (c c') l f k (same as above with Big-O).

Русский

Если f =OWith c l f g и g =OWith c' l g k, тогда f =OWith (c c') l f k.

LaTeX

$$$f = OWith\; c\; l\; f\; g \Rightarrow g = OWith\; c'\; l\; g\; k \Rightarrow f = OWith\; (c c')\; l\; f\; k$$$

Lean4

@[trans]
theorem trans {f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g) (hgk : g =O[l] k) : f =O[l] k :=
  let ⟨_c, cnonneg, hc⟩ := hfg.exists_nonneg
  let ⟨_c', hc'⟩ := hgk.isBigOWith
  (hc.trans hc' cnonneg).isBigO

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