Zulip Chat Archive

Stream: Is there code for X?

Topic: Usual topology on R


view this post on Zulip Bhavik Mehta (Jun 12 2020 at 13:38):

example : topological_space  := by apply_instance

fails for me. What am I doing wrong?

view this post on Zulip Sebastien Gouezel (Jun 12 2020 at 13:39):

What are your imports?

view this post on Zulip Bhavik Mehta (Jun 12 2020 at 13:39):

Currently

import analysis.convex.basic
import topology.subset_properties
import topology.algebra.ordered

view this post on Zulip Bhavik Mehta (Jun 12 2020 at 13:39):

Presumably I need something else

view this post on Zulip Sebastien Gouezel (Jun 12 2020 at 13:42):

import topology.instances.real

noncomputable example : topological_space  := by apply_instance

view this post on Zulip Bhavik Mehta (Jun 12 2020 at 13:42):

Great thanks!


Last updated: May 07 2021 at 18:19 UTC