isLittleO_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 isLittleO_abs_left : (fun x => |u x|) =o[l] g ↔ u =o[l] g :=
  @isLittleO_norm_left _ _ _ _ _ g u l

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