Theorems · Theorem · approximation theory

Asymptotics.isBigO_zero_right_iff

∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {f'' : α → E''} {l : Filter α}, (f'' =O[l] fun _x => 0) ↔ f'' =ᶠ[l] 0

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedAddCommGroup