transEventuallyEqIsBigO — Mathlib

English

The Big-O-with relation is transitive with respect to the pointwise equality relation.

Русский

Отношение IsBigOWith транзитивно по отношению к точечной эквивалентности функций.

LaTeX

$$$ IsBigOWith\; c\; l\; f\; g \;\text{ имеет переход }\; IsBigOWith\; c\; l'\; (f\circ k)\; (g\circ k) $$$

Lean4

instance transEventuallyEqIsBigO : @Trans (α → E) (α → E) (α → F) (· =ᶠ[l] ·) (· =O[l] ·) (· =O[l] ·) where
  trans := Filter.EventuallyEq.trans_isBigO

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