How do I import metric space in Lean Web Editor

Stream: new members

[Lars Ericson]

I am using Lean Web Editor: https://leanprover-community.github.io/lean-web-editor/#

I would like to import metric_space.

Lean Web Editor doesn't seem to know mathlib, in the sense that none of these work:

import topology
import topology.metric_space
import topology.metric_space.basic

All result in the error

file 'topology' not found in the search path
invalid import: topology
could not resolve import: topology

Is there a way to point Lean Web Editor to mathlib?

[Lars Ericson]

Never mind, I figured it out after installing the local editor from this video: https://youtu.be/02ff4WrW0FU

import topology.metric_space.basic

It is a lot easier to use the local editor because it tells you as you're typing what is available. I'm going local from now on!

[Kenny Lau]

wise choice

[Bryan Gin-ge Chen]

For what it's worth, the topology.metric_space.basic import does work for me on the web editor, see here. But yes, the local editor is much, much better!