isBigO_sub — Mathlib

English

Let e be a continuous linear equivalence between normed spaces. Then for any f: α → E and l a filter, the composed map α → F given by x ↦ e(f x) is Big-O of f with respect to l.

Русский

Пусть e — непрерывное линейное эквивалентное отображение между нормированными пространствами. Тогда композиция x ↦ e(f x) является Big-O по отношению к f.

LaTeX

$$$$ (x \\mapsto e(f(x))) =O_l f $$$$

Lean4

theorem isBigO_sub (l : Filter E) (x : E) : (fun x' => e (x' - x)) =O[l] fun x' => x' - x :=
  (e : E →SL[σ₁₂] F).isBigO_sub l x

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