Theorems · Theorem · approximation theory

Asymptotics.IsEquivalent.tendsto_atTop

∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [OrderTopology β],
  Asymptotics.IsEquivalent l u v → Filter.Tendsto u l Filter.atTop → Filter.Tendsto v l Filter.atTop

Defined in

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedFieldLinearOrderIsStrictOrderedRingOrderTopology