Ashwin Iyengar (Feb 12 2021 at 15:14):
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.
Ruben Van de Velde (Feb 12 2021 at 15:28):
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