isLittleO_norm_norm — Mathlib

English

Let α be a type, E' a normed group, F' a normed group, and l a filter. Then IsBigO l (‖f'(x)‖) (g' (x)) is equivalent to IsBigO l f' g'.

Русский

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

LaTeX

$$$IsBigO\\_l( \\|f'\\|, g') \\iff IsBigO\\_l(f', g')$$$

Lean4

theorem isLittleO_norm_norm : ((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) ↔ f' =o[l] g' :=
  isLittleO_norm_left.trans isLittleO_norm_right

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