Zulip Chat Archive

Stream: general

Topic: rewrite doubly defined theorem


view this post on Zulip Ashwin Iyengar (Feb 12 2021 at 15:14):

There's a tendsto_nhds in metric_space/basic.lean and a tendsto_nhds in topology/basic.lean. I'm working with a metric space. When I do rw tendsto_nhds, it performs the topology rewrite, but I want it to do the metric space one. Is there a way to choose? This seems like a scope issue.

view this post on Zulip Ruben Van de Velde (Feb 12 2021 at 15:28):

Try metric.tendsto_nhds?

view this post on Zulip Ashwin Iyengar (Feb 12 2021 at 15:36):

Oh great thanks, I was trying metric_space.tendsto_nhds without looking at what the namespace is called!


Last updated: May 16 2021 at 20:13 UTC