isBigO_comp — Mathlib

English

If g is a bounded linear map F → G and f: α → F, then the map x ↦ g(f(x)) is O of f, i.e., there exists C with ∥g(f(x))∥ ≤ ∥g∥ · ∥f(x)∥ for all x.

Русский

Если g — ограниченное линейное отображение F → G, то отображение x ↦ g(f(x)) есть O(f).

LaTeX

$$$$\\|g(f(x))\\| \\leq \\|g\\| \\cdot \\|f(x)\\| \\quad(\\forall x).$$$$

Lean4

theorem isBigO_comp [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) :
    (fun x' => g (f x')) =O[l] f :=
  (g.isBigOWith_comp f l).isBigO

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