isBigO_const_mul_right_iff'

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigO_const_mul_right_iff'

← MathLib Explorer

English

If c is a unit and IsBigO l f (c·g) then IsBigO l f g.

Русский

Если c — единица и IsBigO l f (c·g), то IsBigO l f g.

LaTeX

$$$\text{IsBigO}(l, f, (c\cdot g)) \iff \text{IsBigO}(l, f, g), \text{ при } c\in\text{Units}.$$$

Lean4

theorem isBigO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) : (f =O[l] fun x => c * g x) ↔ f =O[l] g :=
  ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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