Theorems · Theorem · approximation theory

Asymptotics.isLittleO_one_iff

∀ {α : Type u_1} (F : Type u_4) {E''' : Type u_12} [inst : Norm F] [inst_1 : SeminormedAddGroup E'''] {l : Filter α}
  [inst_2 : One F] [NormOneClass F] {f : α → E'''}, (f =o[l] fun _x => 1) ↔ Filter.Tendsto f l (nhds 0)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

20 results in Mathlib

Foundations

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

Assumes

NormSeminormedAddGroupOneNormOneClass