isBigOWith_abs_left

Mathlib.Analysis.Asymptotics.Defs

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

English

The bound with the left-hand side absolute value is equivalent to the bound with the left-hand side itself.

Русский

Граница слева через модуль равна границе слева через саму величину.

LaTeX

$$$IsBigOWith c l (|u|) f g \iff IsBigOWith c l u f g$$$

Lean4

@[simp]
theorem isBigOWith_abs_left : IsBigOWith c l (fun x => |u x|) g ↔ IsBigOWith c l u g :=
  @isBigOWith_norm_left _ _ _ _ _ _ g u l

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

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

Разделы

Аффилиация

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