Usual topology on R

Stream: Is there code for X?

[Bhavik Mehta]

example : topological_space ℝ := by apply_instance

fails for me. What am I doing wrong?

[Sebastien Gouezel]

What are your imports?

[Bhavik Mehta]

Currently

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

[Bhavik Mehta]

Presumably I need something else

[Sebastien Gouezel]

import topology.instances.real

noncomputable example : topological_space ℝ := by apply_instance

[Bhavik Mehta]

Great thanks!