Picking sides

Stream: maths

[Patrick Massot]

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]

@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]

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

[Patrick Massot]

T2 spaces?

[Patrick Massot]

:grinning:

[Reid Barton]

how about xor?

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

And I also think that defining cluster_pt (x : X) (F : filter X) would help maintaining consistency.

[Reid Barton]

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]

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]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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]

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

[Reid Barton]

I have to say I just kind of assumed that 𝓟 s meant the power set of s without thinking about it

[Reid Barton]

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

[Patrick Massot]

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]

Reid, do you have a better notation?

[Patrick Massot]

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

[Reid Barton]

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

[Patrick Massot]

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]

See #3160.

[Patrick Massot]

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

[Anatole Dedecker]

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]

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]

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]

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]

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

[Patrick Massot]

Sure, but we started with the super elementary approach.