isBigO_of_subsingleton

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigO_of_subsingleton

English

If IsBigOWith c l f g' holds, then there exists c' > 0 with IsBigOWith c' l f g'.

Русский

Если выполняется IsBigOWith c l f g', то существует c' > 0, такое что IsBigOWith c' l f g'.

LaTeX

$$$ IsBigOWith c l f g' \rightarrow \exists c'>0, IsBigOWith c' l f g' $$$

Lean4

@[nontriviality]
theorem isBigO_of_subsingleton [Subsingleton E'] : f' =O[l] g' :=
  isLittleO_of_subsingleton.isBigO

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

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

Разделы

Аффилиация

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