isBigOWith

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.isBigOWith

English

If f = o[l] g, then there exists a real constant c such that f = OWith c l f g; equivalently, ∃ c ∈ ℝ, IsBigOWith c l f g.

Русский

Если f = o[l] g, то существует вещественная константа c, такая что f = IsBigOWith c l f g.

LaTeX

$$$ f =O[l] g \rightarrow \exists c \in \mathbb{R}, IsBigOWith c l f g $$$

Lean4

theorem isBigOWith : f =O[l] g → ∃ c : ℝ, IsBigOWith c l f g :=
  isBigO_iff_isBigOWith.1

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

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

Разделы

Аффилиация

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