isLittleO_abs_abs — Mathlib

English

Let α be a type, E' a normed space, F' a normed space, and l a filter. Then ((‖f'(x)‖) = o_l (‖g'(x)‖)) iff f' = o_l g'.

Русский

Пусть α — тип; f' : α → E', g' : α → F'; тогда (‖f'(x)‖) = o_l (‖g'(x)‖) эквивалентно f' = o_l g'.

LaTeX

$$$((x \\mapsto \\|f'(x)\\|)) =o_l (g'(x)) \\iff f' =o_l g'$$$

Lean4

theorem isLittleO_abs_abs : ((fun x => |u x|) =o[l] fun x => |v x|) ↔ u =o[l] v :=
  isLittleO_abs_left.trans isLittleO_abs_right

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