const_mul_right

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.const_mul_right

← MathLib Explorer

English

If c is a unit, then IsLittleO l f (c·g) iff IsLittleO l f g.

Русский

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

LaTeX

$$$\text{IsLittleO}(l, f, (c\cdot g)) \iff \text{IsLittleO}(l, f, g), \text{ при } c \text{ единица}.$$$

Lean4

theorem const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) (h : f =o[l] g) : f =o[l] fun x => c * g x :=
  h.trans_isBigO <| isBigO_self_const_mul hc g l

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

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

Разделы

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

Аффилиация

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