isBigO_const_one

Mathlib.Analysis.Asymptotics.Lemmas

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

English

The bound IsBigOWith ‖c‖ l cst with a constant c equals IsBigOWith ‖c‖ l with the constant 1 on the same bound.

Русский

Bound IsBigOWith ‖c‖ l с константой сохраняется при переходе к константе 1.

LaTeX

$$IsBigOWith ‖c‖ l f g ↔ IsBigOWith ‖c‖ l f g$$

Lean4

theorem isBigO_const_one (c : E) (l : Filter α) : (fun _x : α => c) =O[l] fun _x => (1 : F) :=
  (isBigOWith_const_one F c l).isBigO

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

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

Разделы

Аффилиация

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