Theorems · Theorem · approximation theory

Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

∀ {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [inst : SeminormedAddCommGroup E'] [inst_1 : NormedDivisionRing 𝕜]
  [inst_2 : Module 𝕜 E'] [NormSMulClass 𝕜 E'] {f : α → E'} {g : α → 𝕜} {l : Filter α},
  f =o[l] g → Filter.Tendsto (fun x => (g x)⁻¹ • f x) l (nhds 0)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedDivisionRingModuleNormSMulClass