Zulip Chat Archive

Stream: Is there code for X?

Topic: Usual topology on R


Bhavik Mehta (Jun 12 2020 at 13:38):

example : topological_space  := by apply_instance

fails for me. What am I doing wrong?

Sebastien Gouezel (Jun 12 2020 at 13:39):

What are your imports?

Bhavik Mehta (Jun 12 2020 at 13:39):

Currently

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

Bhavik Mehta (Jun 12 2020 at 13:39):

Presumably I need something else

Sebastien Gouezel (Jun 12 2020 at 13:42):

import topology.instances.real

noncomputable example : topological_space  := by apply_instance

Bhavik Mehta (Jun 12 2020 at 13:42):

Great thanks!


Last updated: Dec 20 2023 at 11:08 UTC