isBigOWith_const_one

Mathlib.Analysis.Asymptotics.Lemmas

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

English

For a nonzero constant c, (f =o[l] c) is equivalent to (f =o[l] 1).

Русский

Для ненулевой константы c: f =o[l] c эквивалентно f =o[l] 1.

LaTeX

$$$(f =o[l] c) \iff (f =o[l] 1)$ при hc ≠ 0$$

Lean4

theorem isBigOWith_const_one (c : E) (l : Filter α) : IsBigOWith ‖c‖ l (fun _x : α => c) fun _x => (1 : F) := by
  simp [isBigOWith_iff]

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

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

Разделы

Аффилиация

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