Theorems · Theorem · functional analysis

Asymptotics.IsLittleOTVS.tendsto_inv_smul

∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E},
  g =o[𝕜; l] f → Filter.Tendsto (fun x => (f x)⁻¹ • g x) l (nhds 0)

Defined in

Mathlib.Analysis.Asymptotics.TVS

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupTopologicalSpaceModuleContinuousSMul