Theorems · Theorem · approximation theory

Filter.Tendsto.isBigO_one

∀ {α : Type u_1} (F : Type u_4) {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {f' : α → E'}
  {l : Filter α} [inst_2 : One F] [NormOneClass F] {c : E'}, Filter.Tendsto f' l (nhds c) → f' =O[l] fun _x => 1

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormSeminormedAddCommGroupOneNormOneClass