## Stream: new members

### Topic: How do I import metric space in Lean Web Editor

#### Lars Ericson (Dec 02 2020 at 04:17):

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 (Dec 02 2020 at 04:29):

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!

wise choice

#### Bryan Gin-ge Chen (Dec 02 2020 at 04:58):

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!

Last updated: May 11 2021 at 13:22 UTC