Theorems · Theorem · approximation theory

Asymptotics.isLittleO_const_iff_isLittleO_one

∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [inst : Norm E] [inst_1 : Norm F]
  [inst_2 : NormedAddCommGroup F''] {f : α → E} {l : Filter α} [inst_3 : One F] [NormOneClass F] {c : F''},
  c ≠ 0 → ((f =o[l] fun _x => c) ↔ f =o[l] fun _x => 1)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormNormNormedAddCommGroupOneNormOneClass