Theorems · Theorem · approximation theory

Asymptotics.div_isBoundedUnder_of_isBigO

∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜},
  f =O[l] g → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedDivisionRing