Theorems · Theorem · functional analysis

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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {α : Type u_7}
  (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α), (fun x' => g (f x')) =O[l] f

Defined in

Mathlib.Analysis.Normed.Operator.Asymptotics

Cited by

4 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceNormedSpaceRingHomIsometric