isBigO

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.isBigO

English

IsBigOTVS implies IsBigO, and conversely IsBigO implies IsBigOTVS when combined with Theta structure.

Русский

IsBigOTVS ⇒ IsBigO и обратно IsBigO ⇒ IsBigOTVS при учете Theta-структуры.

LaTeX

$$$ f =O[l] g \Rightarrow f =BigO[l] g \text{ and } g =O[l] f \Rightarrow f =Θ[l] g. $$$

Lean4

theorem isBigO (h : f =Θ[l] g) : f =O[l] g :=
  h.1

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

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

Разделы

Аффилиация

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