Rohan Mitta (Sep 24 2018 at 19:10):
I'm trying to use the squeeze theorem (tendsto_of_tendsto_of_tendsto_of_le_of_le from topological_structures) on a sequence from the naturals to the reals, but I get the error failed to synthesize type class instance for orderable_topology \N
What should I do?
Rohan Mitta (Sep 24 2018 at 19:14):
Sorry, ignore this, I made a silly mistake
Last updated: Aug 03 2023 at 10:10 UTC