Theorems · Theorem · approximation theory

Asymptotics.IsEquivalent.mono

∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {f g : α → β} {l' : Filter α},
  Asymptotics.IsEquivalent l' f g → l ≤ l' → Asymptotics.IsEquivalent l f g

Defined in: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Cited by: 0 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

NormedAddCommGroupstatement and proof · cited by 15,752
Filterstatement and proof · cited by 8,121
Asymptotics.IsEquivalentstatement and proof · cited by 98
Asymptotics.IsLittleO.monoproof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.