isBigO_sub — Mathlib

English

For a bounded linear map f, the quantity f(x) grows at most like x when x varies; i.e., (fun x' => f(x' - x)) =O[l] (fun x' => x' - x) for any l on E.

Русский

Для ограниченного линейного отображения f величина f(x) растет не быстрее x; то есть (fun x' => f(x' - x)) =O[l] (fun x' => x' - x).

LaTeX

$$$IsBoundedLinearMap\ 𝕜\ f\rightarrow (\lambda x'\,=>\,f(x'-x))=O[l](\lambda x'\,=>\,x'-x)$$$

Lean4

theorem isBigO_sub {f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) (x : E) :
    (fun x' => f (x' - x)) =O[l] fun x' => x' - x :=
  isBigO_comp h l

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