# Zulip Chat Archive

## Stream: new members

### Topic: Jay Williams

#### Jay Williams (Sep 27 2020 at 22:14):

Hi all,

I've been playing around with Lean lately, working through the natural number game and the tutorials project. I used to study descriptive set theory, and I thought I might try to prove some of the basics in Lean. There is a lot of overlap between basic point-set topology and basic descriptive set theory, so a lot of useful stuff is already in `mathlib`

, but there are still plenty of things that aren't there yet. My hope is that I can do some of the easy stuff in my free time. :)

I realized that for all the information included in the tutorials project, I still don't know how to do something as basic as define a Polish space (a completely metrizable and separable topological space). There are at least two aspects to this:

a) I'm not sure if it's better to define a Polish space as a metric space or a topological space, i.e. I'm not sure the "correct" way to work with metrizable spaces. Some of the proofs I'd like to do definitely use the metric, though of course there may be some other way to do them.

b) Even if I just decided "okay, I'll just say it's a complete and separable space for now to get started", I'm not sure how to do that. I can find a few similar definitions in `mathlib`

such as that of a `borel_space`

, but I'm not really sure how the `class`

keyword works (for example), and of course most of these files start with a lot of boilerplate that I don't yet understand the significance of.

So if anyone can point me at some relevant docs or examples, that would be excellent. I'm looking forward to getting something proved, even if it's small.

#### Mario Carneiro (Sep 27 2020 at 22:17):

If a Polish space is metrizable, then I guess you should say that; that is, it should not come with a metric

#### Mario Carneiro (Sep 27 2020 at 22:17):

Also hello

#### Mario Carneiro (Sep 27 2020 at 22:19):

As for examples, perhaps something like docs#topological_space.first_countable_topology can get you started? Definition making is one of the more complicated things to do in lean without prior expertise, because it shapes a lot of what comes later and there are sometimes subtle details that relate more to the way lean works than the way the mathematics works

#### Heather Macbeth (Sep 27 2020 at 22:20):

Welcome!

Jay Williams said:

b) Even if I just decided "okay, I'll just say it's a complete and separable space for now to get started", I'm not sure how to do that. I can find a few similar definitions in

`mathlib`

such as that of a`borel_space`

, but I'm not really sure how the`class`

keyword works (for example), and of course most of these files start with a lot of boilerplate that I don't yet understand the significance of.

This seems a reasonable way to start. Perhaps you could state (in words) a lemma, then someone here can give you the Lean statement and you can start playing with the proof.

#### Mario Carneiro (Sep 27 2020 at 22:24):

The `class`

keyword is just a synonym for `@[class] structure`

, so if you know how the structure keyword works then class is no different. (Of course that might not be any help.)

#### Jay Williams (Sep 27 2020 at 22:25):

Heather Macbeth said:

This seems a reasonable way to start. Perhaps you could state (in words) a lemma, then someone here can give you the Lean statement and you can start playing with the proof.

Ah this is a great idea, I think I was getting ahead of myself a little bit. Well let's see, the very first things in Kechris' _Descriptive Set Theory_ that are proved about Polish spaces are

- The completion of a separable metric space is Polish.
- A closed subspace of a Polish space is Polish.

#### Kenny Lau (Sep 27 2020 at 22:26):

Learning Lean is like picking up a new language -- you just try out things until they work

#### Mario Carneiro (Sep 27 2020 at 22:26):

One thing you don't need any particular lean expertise to do is unpack all the words until everything is in terms of concepts in mathlib

#### Jay Williams (Sep 27 2020 at 22:27):

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

#### Heather Macbeth (Sep 27 2020 at 22:28):

Jay Williams said:

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

So if we do this with your (1), is the point that the completion of a separable metric space is separable?

#### Mario Carneiro (Sep 27 2020 at 22:28):

you can of course define "Polish space" to mean that, and then you can use Polish space

#### Mario Carneiro (Sep 27 2020 at 22:28):

but the point is to define anything you need along the way

#### Jay Williams (Sep 27 2020 at 22:29):

Heather Macbeth said:

Jay Williams said:

Ah so rather than worrying about including the words "Polish space" just do the above lemmas with "complete and separable space". That's a good idea!

So if we do this with your (1), is the point that the completion of a separable metric space is separable?

That's right, that's why it's the very first thing, it's almost immediate.

#### Mario Carneiro (Sep 27 2020 at 22:29):

I suppose immediacy is in the eye of the beholder

#### Jay Williams (Sep 27 2020 at 22:30):

As learning Lean is teaching me :)

#### Heather Macbeth (Sep 27 2020 at 22:31):

So I think this would be something like

```
instance it_begins {X : Type*} [metric_space X] [separable_space X] :
separable_space (completion X) :=
begin
sorry
end
```

(not checked in vscode) (updated, thanks @Kenny Lau )

#### Kenny Lau (Sep 27 2020 at 22:31):

`instance`

#### Kenny Lau (Sep 27 2020 at 22:34):

I suppose it is obvious :P

#### Heather Macbeth (Sep 27 2020 at 22:34):

Kenny Lau said:

I suppose it is obvious :P

All the better, for a beginner!

#### Kenny Lau (Sep 27 2020 at 22:34):

oh, I just meant mathematically

#### Kenny Lau (Sep 27 2020 at 22:35):

and that translates to easy in Lean if you prove the right lemmas

#### Mario Carneiro (Sep 27 2020 at 22:35):

which is of course the hard part

#### Jay Williams (Sep 27 2020 at 22:36):

Yes, this is definitely a great start. I'm trying it out now and discovering that I don't quite have my Lean environment set up correctly. The fun part of programming ha. But I will work on this, thanks!

#### Heather Macbeth (Sep 27 2020 at 22:41):

And then when you succeed you should PR it! :smiley:

https://leanprover-community.github.io/contribute/index.html

#### Yury G. Kudryashov (Sep 27 2020 at 22:50):

And see if it works for a `[emetric_space]`

instead of a `[metric_space]`

.

#### Yury G. Kudryashov (Sep 27 2020 at 22:51):

BTW, do we use `[separable_space]`

or `[second_countable_topology]`

as a "normal form" of assumption for a `[emetric_space]`

?

#### Yury G. Kudryashov (Sep 27 2020 at 22:52):

Measure theory assumes `[second_countable_topology]`

in many lemmas and definitions.

#### Jay Williams (Sep 27 2020 at 22:52):

Actually, this is a bit embarrassing, but I can't figure out the `import`

for `separable_space`

. I see that the definition is in `topology/bases.lean`

, but when I try

```
import topology.metric_space.basic
import topology.uniform_space.completion
import topology.bases
instance it_begins {X : Type*} [metric_space X] [separable_space X] :
separable_space (completion X) :=
begin
sorry
end
```

I get red squigglies underneath `separable_space`

.

#### Yury G. Kudryashov (Sep 27 2020 at 22:53):

Please add a newline after the first "```"

#### Jay Williams (Sep 27 2020 at 22:53):

In a metrizable space separability and second countability are equivalent, so I'm fine with either.

#### Yury G. Kudryashov (Sep 27 2020 at 22:53):

Possibly it is in the `topological_space`

namespace

#### Yury G. Kudryashov (Sep 27 2020 at 22:54):

So you can either write `topological_space.separable_space`

, or `open topological_space`

#### Jay Williams (Sep 27 2020 at 22:55):

That worked, though it turns out I have the wrong import for the completion... one thing at a time I guess :smile:

#### Yury G. Kudryashov (Sep 27 2020 at 22:55):

I think that we don't have many theorems about metrizable topological spaces because we didn't have to work with metrizable spaces with no natural `[emetric_space]`

structure.

#### Yury G. Kudryashov (Sep 27 2020 at 22:56):

Try `topology/metric_space/completion`

.

#### Jay Williams (Sep 27 2020 at 22:56):

Certainly the important examples in descriptive set theory all have natural metrics (Baire space, Cantor space, the reals...)

#### Yury G. Kudryashov (Sep 27 2020 at 22:59):

It's easy to define (untested)

```
class metrizable (α : Type*) [h : topological_space α] :=
(metrizable : ∃ β : emetric_space α, β.to_topological_space = h)
```

But every proof about `[metrizable α]`

will start with

```
begin
letI : emetric_space α := ...,
end
```

#### Yury G. Kudryashov (Sep 27 2020 at 23:04):

Here `...`

should be a function that returns a `emetric_space α`

instance such that `emetric_space.to_topological_space = h`

is a definitional equality.

#### Jay Williams (Sep 27 2020 at 23:05):

This still doesn't like `completion`

:

```
import topology.metric_space.basic
import topology.metric_space.completion
open topological_space
instance it_begins {X : Type*} [metric_space X] [separable_space X] :
separable_space (completion X) :=
begin
sorry
end
```

I've tried a few variants, including with some additional stuff in `open`

, but nothing is working... :thinking:

#### Yury G. Kudryashov (Sep 27 2020 at 23:07):

Let me guess docs#completion.completion

#### Yury G. Kudryashov (Sep 27 2020 at 23:09):

So, it should be `open topological_space uniform_space`

#### Jay Williams (Sep 27 2020 at 23:10):

oh geez, I thought I tried that one. Thanks!

#### Jay Williams (Sep 27 2020 at 23:11):

I'm going to have to read up on `open`

, sounds like.

#### Heather Macbeth (Sep 27 2020 at 23:19):

You won't need to read very much. :) When you need a lemma or definition, check the docs (or scroll up in the source) to find the `namespace`

it's in, then `open`

that namespace in your code. Here: docs#uniform_space.completion .

#### Heather Macbeth (Sep 27 2020 at 23:27):

Also, @Jay Williams there's a bad omission in the stub I gave you -- should have been (note the `⟨ ... ⟩`

)

```
import topology.bases
import topology.metric_space.completion
open topological_space uniform_space
instance it_begins {X : Type*} [metric_space X] [separable_space X] :
separable_space (completion X) :=
⟨ begin
sorry
end ⟩
```

#### Yury G. Kudryashov (Sep 27 2020 at 23:33):

I think that the implication should work for any uniform embedding of uniform spaces (just use the image of a fence sequence)

#### Yury G. Kudryashov (Sep 27 2020 at 23:35):

Or even for a dense embedding of topological spaces

#### Aaron Anderson (Sep 28 2020 at 03:04):

Is it possible that a complete metric space is equivalent to a complete uniform space?

#### Yury G. Kudryashov (Sep 28 2020 at 03:48):

What exactly do you mean?

#### Aaron Anderson (Sep 28 2020 at 03:59):

So, one of the aspects of a Polish space is the existence of a complete metric that’s compatible with the topology

#### Aaron Anderson (Sep 28 2020 at 04:00):

I went looking for the definition of a complete metric in mathlib, but I only found `complete space`

which is a uniform space definition

#### Aaron Anderson (Sep 28 2020 at 04:00):

I guess I have two questions:

#### Aaron Anderson (Sep 28 2020 at 04:01):

If you have a metric space, is completeness of that metric space equivalent to completeness of the uniform space?

#### Aaron Anderson (Sep 28 2020 at 04:02):

If you have a complete uniform space that doesn’t necessarily come from a metric, does there exist a (not necessarily unique) complete metric inducing the same topology?

#### Aaron Anderson (Sep 28 2020 at 04:03):

(I know some things about basic descriptive set theory, but have yet to study Lean’s topology and analysis libraries, and know little about uniform spaces)

#### Yury G. Kudryashov (Sep 28 2020 at 06:05):

We define completeness in terms of `uniform_space`

structure. Completeness of `(e)metric_space`

s uses this definition. For a metric space, it is equivalent to the usual definition, see docs#metric.complete_of_cauchy_seq_tendsto and docs#metric.cauchy_seq_iff

#### Yury G. Kudryashov (Sep 28 2020 at 06:07):

Wiki says the following about metrizability: https://en.wikipedia.org/wiki/Nagata%E2%80%93Smirnov_metrization_theorem

#### Patrick Massot (Sep 28 2020 at 07:46):

Some precisions:

- I think a complete uniform space is not necessarily metrizable, even if it is separated
- We don't have this Nagata-Smirnov theorem, and I don't think anyone is interested in this up to now
- We do have https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/compact_separated.html which is somewhat in the same thread

Last updated: Dec 20 2023 at 11:08 UTC