leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: Orderable Topology on Naturals


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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll