Theorems · Theorem · approximation theory

Asymptotics.isLittleO_const_smul_left

∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module 𝕜 E'] [NormSMulClass 𝕜 E']
  {c : 𝕜}, c ≠ 0 → ((fun x => c • f' x) =o[l] g ↔ f' =o[l] g)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormSeminormedAddCommGroupNormedDivisionRingModuleNormSMulClass