English
If a function f is small relative to g and g is small relative to h with respect to the same asymptotic framework, then f is small relative to h. In other words, the transitive property holds for the IsLittleOTVS relation.
Русский
Если функция f относится как мало по отношению к g и функция g относится как мало по отношению к h относительно той же асимптотической структуры, то и f относится как мало по отношению к h. Иначе говоря, выполняется транзитивность для отношения IsLittleOTVS.
LaTeX
$$$\\text{If } f =_{{\\mathfrak{k}}; l\\;\\text{IsLittleOTVS } f \\; g \\text{ and } g =_{{\\mathfrak{k}}; l\\;\\text{IsLittleOTVS } g \\; h, \\text{ then } f =_{{\\mathfrak{k}}; l\\;\\text{IsLittleOTVS } f \\; h}.$$$
Lean4
instance instTransIsLittleOTVSIsLittleOTVS :
@Trans (α → E) (α → F) (α → G) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) (IsLittleOTVS 𝕜 l) where
trans := IsLittleOTVS.trans
