Theorems · Theorem · approximation theory

Asymptotics.isBigO_one_nhds_ne_iff

∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} [inst_2 : One F]
  [NormOneClass F] [inst_4 : TopologicalSpace α] {a : α}, (f =O[nhdsWithin a {a}ᶜ] fun x => 1) ↔ f =O[nhds a] fun x => 1

The condition f = O[𝓝[≠] a] 1 is equivalent to f = O[𝓝 a] 1.

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormNormOneNormOneClassTopologicalSpace