∀ {α : 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.atBot ↔ Filter.Tendsto v l Filter.atBot)