isBigOWith_neg_right

Mathlib.Analysis.Asymptotics.Defs

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

English

Let α be a type, E' a normed space, F' a normed space, and l a filter. Then (abs u) = o_l g iff u = o_l g, for real u.

Русский

Пусть α — тип; u: α → ℝ; g: α → F'. Тогда abs(u) = o_l g эквивалентно u = o_l g.

LaTeX

$$$(|u|) =o_l g \\iff u =o_l g$$

Lean4

@[simp]
theorem isBigOWith_neg_right : (IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g' := by
  simp only [IsBigOWith_def, norm_neg]

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

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

Разделы

Аффилиация

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