Zulip Chat Archive

Stream: maths

Topic: Picking sides


view this post on Zulip 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  }

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 24 2020 at 19:06):

Does 𝓝 _ ⊓ _ or _ ⊓ 𝓝 _ appear elsewhere?

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:08):

T2 spaces?

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:08):

:grinning:

view this post on Zulip Reid Barton (Jun 24 2020 at 19:14):

how about xor?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:17):

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

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:18):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 19:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jun 24 2020 at 19:42):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 24 2020 at 19:52):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:53):

Reid, do you have a better notation?

view this post on Zulip Patrick Massot (Jun 24 2020 at 19:58):

In order.filter.basic alone, principal appears 139 times...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 24 2020 at 23:14):

See #3160.

view this post on Zulip Patrick Massot (Jun 24 2020 at 23:15):

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

view this post on Zulip 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:

view this post on Zulip 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).

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jun 25 2020 at 19:44):

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

view this post on Zulip 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