ContinuousLinearMap.isBigO_comp

theorem ContinuousLinearMap.isBigO_comp : ∀ {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_5} {G : Type u_6} [inst : SeminormedAddCommGroup F] [inst_1 : SeminormedAddCommGroup G] [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NontriviallyNormedField 𝕜₃] [inst_4 : NormedSpace 𝕜₂ F] [inst_5 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [inst_6 : RingHomIsometric σ₂₃] {α : Type u_7} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α), (fun x' => g (f x')) =O[l] f

This theorem states that, for all types `𝕜₂`, `𝕜₃`, `F`, `G`, and `α`, given a continuous linear map `g` from `F` to `G` over a ring homomorphism `σ₂₃` from `𝕜₂` to `𝕜₃`, and a function `f` from `α` to `F`, with `l` as a filter on `α`, the composition function `(fun x' => g (f x'))` is a big O of function `f` at filter `l`. Here "big O" notation is a mathematical notation used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, usually in terms of simpler functions.

More concisely: For any types `𝕜₂`, `𝕜₃`, `F`, `G`, `α`, given a continuous linear map `g` from `F` to `G` over a ring homomorphism `σ₂₃` from `𝕜₂` to `𝕜₃`, and a function `f` from `α` to `F`, the composition `g ∘ f` is a big O of `f` with respect to filter `l` on `α`.