isBigO_abs_left — Mathlib

English

Let α be a type, E' a normed space, F' a normed space, and l a filter on α. For any u: α → Real and g: α → F', we have (x ↦ |u(x)|) =O_l g if and only if u =O_l g.

Русский

Пусть α — тип, u: α → ℝ и g: α → F' (F' нормированное пространство). Тогда x ↦ |u(x)| есть O_l(g) тогда и только тогда, когда u = O_l(g).

LaTeX

$$$\\bigl(x \\mapsto |u(x)|\\bigr) =O_l\\ g \\iff u =O_l\\ g$$

Lean4

@[simp]
theorem isBigO_abs_left : (fun x => |u x|) =O[l] g ↔ u =O[l] g :=
  @isBigO_norm_left _ _ _ _ _ g u l

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