Theorems · Theorem · approximation theory

Asymptotics.IsBigO.inv_rev

∀ {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜']
  {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'},
  f =O[l] g → (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → (fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingNormedDivisionRing