trans

Mathlib.Analysis.Asymptotics.TVS

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleOTVS.trans

English

IsLittleOTVS transitivity to IsBigOTVS via a chain

Русский

IsLittleOTVS через цепочку к IsBigOTVS

LaTeX

$$trans_isBigOTVS: $f =o_{𝕜;l} g \\land g =O_{𝕜;l} k \\Rightarrow f =o_{𝕜;l} k$$$

Lean4

@[trans]
theorem trans {k : α → G} (hfg : f =o[𝕜; l] g) (hgk : g =o[𝕜; l] k) : f =o[𝕜; l] k :=
  hfg.trans_isBigOTVS hgk.isBigOTVS

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru