transIsBigOIsLittleO — Mathlib

English

Element of a transitive chain connecting LittleO relations: LittleO trans to LittleO.

Русский

Элемент транзитной цепи, соединяющий отношения LittleO: LittleO переходит в LittleO.

LaTeX

$$IsLittleO l f g \land IsLittleO l g k \Rightarrow IsLittleO l f k$$

Lean4

instance transIsBigOIsLittleO : @Trans (α → E) (α → F') (α → G) (· =O[l] ·) (· =o[l] ·) (· =o[l] ·) where
  trans := IsBigO.trans_isLittleO

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