Theorems · Theorem · approximation theory

Asymptotics.isLittleO_principal

∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {g' : α → F'} {f'' : α → E''} {s : Set α}, f'' =o[Filter.principal s] g' ↔ ∀ x ∈ s, f'' x = 0

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedAddCommGroup