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