# Zulip Chat Archive

## Stream: maths

### Topic: Picking sides

#### Patrick Massot (Jun 24 2020 at 19:02):

Consider the following lemmas from mathlib:

```
variables {α : Type*} [topological_space α]
cluster_point_of_compact [compact_space α] {f : filter α} : f ≠ ⊥ → ∃ x, f ⊓ 𝓝 x ≠ ⊥
closure_eq_nhds {s : set α}, closure s = {a : α | 𝓝 a ⊓ 𝓟 s ≠ ⊥}
```

#### Patrick Massot (Jun 24 2020 at 19:03):

@Yury G. Kudryashov @Reid Barton is there are reason to keep this discrepancy? I think it causes quite a few `rw inf_comm`

down the road.

#### Reid Barton (Jun 24 2020 at 19:06):

Does `𝓝 _ ⊓ _`

or `_ ⊓ 𝓝 _`

appear elsewhere?

#### Patrick Massot (Jun 24 2020 at 19:08):

T2 spaces?

#### Patrick Massot (Jun 24 2020 at 19:08):

:grinning:

#### Reid Barton (Jun 24 2020 at 19:14):

how about xor?

#### Reid Barton (Jun 24 2020 at 19:15):

If I wrote either of these, I don't remember picking the order for any particular reason.

#### Patrick Massot (Jun 24 2020 at 19:17):

`def nhds_within (a : α) (s : set α) : filter α := 𝓝 a ⊓ principal s`

#### Patrick Massot (Jun 24 2020 at 19:18):

As far as I can see, all occurrences are linked to one of these three sources.

#### Patrick Massot (Jun 24 2020 at 19:18):

I don't claim you wrote any of these, I only pinged people who care about topology and were online at that time.

#### Patrick Massot (Jun 24 2020 at 19:19):

I think changing the order used in the definition of compact would be less work.

#### Patrick Massot (Jun 24 2020 at 19:21):

And I also think that defining `cluster_pt (x : X) (F : filter X)`

would help maintaining consistency.

#### Reid Barton (Jun 24 2020 at 19:24):

I think that would help with readability too. I have to think a lot about `f ⊓ 𝓝 x ≠ ⊥`

but I have at least some intuition for cluster points of filters.

#### Patrick Massot (Jun 24 2020 at 19:30):

I'm the worst enemy of the sphere eversion project. Each day I swear I'll work on it I find some tiny mathlib hole to fill and it turns into giant refactoring.

#### Patrick Massot (Jun 24 2020 at 19:36):

Of course this will also impact my recent work on subsequences, where I was already fighting this discrepancy.

#### Patrick Massot (Jun 24 2020 at 19:38):

Patrick Massot said:

I'm the worst enemy of the sphere eversion project. Each day I swear I'll work on it I find some tiny mathlib hole to fill and it turns into giant refactoring.

What happened today is I pushed heine-4, I was writting the PR message and I thought: really I should prove that extra theorem before I forgot all about this. And I fell into a new rabbit hole.

#### Kevin Buzzard (Jun 24 2020 at 19:40):

I think this is a really good use of projects like this -- they test the library

#### Kevin Buzzard (Jun 24 2020 at 19:40):

But this time you've learnt that the correct thing to do is to fix the library. `for_mathlib`

directories considered harmful.

#### Kevin Buzzard (Jun 24 2020 at 19:41):

I'll get back to schemes over the summer and will hopefully be doing the same sort of thing

#### Yury G. Kudryashov (Jun 24 2020 at 19:42):

I think that it should be normalized to "nhds first".

#### Patrick Massot (Jun 24 2020 at 19:47):

Since I'm a refactoring mood, is there any objection to having notation \MCP for `filter.principal`

? This appears in more than 250 lines of mathlib without notation.

#### Sebastien Gouezel (Jun 24 2020 at 19:49):

Since `principal s`

is already completely obscure :grinning_face_with_smiling_eyes: , the notation can only help here!

#### Reid Barton (Jun 24 2020 at 19:51):

I have to say I just kind of assumed that `𝓟 s`

meant the power set of `s`

without thinking about it

#### Reid Barton (Jun 24 2020 at 19:52):

Obviously, any amount of contemplation would have shown that this is wrong

#### Patrick Massot (Jun 24 2020 at 19:53):

Kevin Buzzard said:

I think this is a really good use of projects like this -- they test the library

Actually, the Heine PR series has nothing to do with this project. It's because of https://leanprover-community.github.io/undergrad_todo.html. Also it's a bit ridiculous that I asked my students to prove the Heine theorem in Lean at the end of my exam (for function on segments of reals numbers of course) but it's not in mathlib.

#### Patrick Massot (Jun 24 2020 at 19:53):

Reid, do you have a better notation?

#### Patrick Massot (Jun 24 2020 at 19:58):

In order.filter.basic alone, `principal`

appears 139 times...

#### Reid Barton (Jun 24 2020 at 20:15):

I don't have a better suggestion. If the notation is localized to topology, I think it's unambiguous enough.

#### Patrick Massot (Jun 24 2020 at 21:36):

I'm fixing all the breakage in compactness stuff from switching sides. It's amazing how defining `cluster_pt`

and proving a handful of lemmas about it shortens many proofs.

#### Patrick Massot (Jun 24 2020 at 23:14):

See #3160.

#### Patrick Massot (Jun 24 2020 at 23:15):

We need to merge that one really fast, because it touches 33 files...

#### Anatole Dedecker (Jun 25 2020 at 17:17):

Patrick Massot said:

Kevin Buzzard said:

I think this is a really good use of projects like this -- they test the library

Actually, the Heine PR series has nothing to do with this project. It's because of https://leanprover-community.github.io/undergrad_todo.html. Also it's a bit ridiculous that I asked my students to prove the Heine theorem in Lean at the end of my exam (for function on segments of reals numbers of course) but it's not in mathlib.

Patrick Massot said:

Kevin Buzzard said:

I think this is a really good use of projects like this -- they test the library

Actually, the Heine PR series has nothing to do with this project. It's because of https://leanprover-community.github.io/undergrad_todo.html. Also it's a bit ridiculous that I asked my students to prove the Heine theorem in Lean at the end of my exam (for function on segments of reals numbers of course) but it's not in mathlib.

Wait Heine isn't in Mathlib ? Also, I'm keeping this page in a bookmark, that's another idea of things to do this summer :laughing:

#### Patrick Massot (Jun 25 2020 at 17:52):

Anatole Dedecker said:

Wait Heine isn't in Mathlib ? Also, I'm keeping this page in a bookmark, that's another idea of things to do this summer :laughing:

We could have put the elementary version a long time ago. But doing the general case requires more work, and nobody has needed it up to now. The main reason why this theorem is taught very early is because it's useful in order to construct Riemann integration. mathlib jumped over this and went straight to Lebesgue (and even Bochner actually).

#### Anatole Dedecker (Jun 25 2020 at 18:56):

Patrick Massot said:

Anatole Dedecker said:

Wait Heine isn't in Mathlib ? Also, I'm keeping this page in a bookmark, that's another idea of things to do this summer :laughing:

We could have put the elementary version a long time ago. But doing the general case requires more work, and nobody has needed it up to now. The main reason why this theorem is taught very early is because it's useful in order to construct Riemann integration. mathlib jumped over this and went straight to Lebesgue (and even Bochner actually).

Yeah I see. In general, would it be a good idea to actually put such specializations first in the library, or do you recommend always starting by the general case ?

#### Patrick Massot (Jun 25 2020 at 18:57):

We usually start with the general case, but there are exceptions. For instance, the file defining exponential and trigonometric functions is *very* elementary.

#### Sebastien Gouezel (Jun 25 2020 at 19:44):

Yes, but hopefully it won't stay like that forever.

#### Patrick Massot (Jun 25 2020 at 19:45):

Sure, but we started with the super elementary approach.

Last updated: May 18 2021 at 08:14 UTC