Zulip Chat Archive

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!

Kenny Lau (Dec 02 2020 at 04:31):

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: Dec 20 2023 at 11:08 UTC