exists_nonneg

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigOWith.exists_nonneg

English

If f = O[l] g, then there exists c > 0 such that f = OWith c l f g.

Русский

Если f = O[l] g, то существует c > 0 с таким свойством, что f = OWith c l f g.

LaTeX

$$$ f =O[l] g \rightarrow \exists c > 0, IsBigOWith c l f g $$$

Lean4

theorem exists_nonneg (h : IsBigOWith c l f g') : ∃ c' ≥ 0, IsBigOWith c' l f g' :=
  let ⟨c, cpos, hc⟩ := h.exists_pos
  ⟨c, le_of_lt cpos, hc⟩

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

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

Разделы

Аффилиация

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