isBigOWith_norm_norm — Mathlib

English

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

Русский

Пусть α — множество; E', F' — нормы; c ∈ ℝ; l — фильтр. Тогда IsBigOWith(c,l,‖f'‖,‖g'‖) эквивалентно IsBigOWith(c,l,f',g').

LaTeX

$$$\\operatorname{IsBigOWith}(c,l,\\|f'\\|,\\|g'\\|) \\iff \\operatorname{IsBigOWith}(c,l,f',g')$$$

Lean4

theorem isBigOWith_norm_norm : (IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) ↔ IsBigOWith c l f' g' :=
  isBigOWith_norm_left.trans isBigOWith_norm_right

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