Characterization of closed subspace

Stream: Is there code for X?

[Heather Macbeth]

To prove a subset of a topological space is closed, it suffices to prove that limits of sequences (filters?) of elements of the subset are in the subset. [Where] is this in mathlib?

I can find the converse: docs#is_closed.mem_of_tendsto

[Adam Topaz]

There's docs#mem_closure_iff_ultrafilter

[Adam Topaz]

And docs#is_closed.closure_eq

[Adam Topaz]

Actually you can probably just use docs#is_closed_iff_cluster_pt

[Kevin Buzzard]

If I click on that docs link that Adam posted (Firefox, Ubuntu, laptop with small screen), I get this:
non_mem_ultrafilter.png
What is happening is that there is a "mathlib documentation topology.basic search" box, which is covering up the actual is_closed.mem_of_tendsto definition. Am I doing something wrong?

[Heather Macbeth]

Adam Topaz said:

Actually you can probably just use docs#is_closed_iff_cluster_pt

Thanks! This one looks like the closest to what I was thinking of.

[Kevin Buzzard]

If I hit reload on my browser the problem does not go away, but if I highlight the URL and hit enter, it works fine.

[Adam Topaz]

I have the same issue

[Adam Topaz]

But if I open the link in chromium, the issue disappears. (So it might be a firefox thing...)

[Kevin Buzzard]

I'll open an issue. What's your OS? And do you know what repo to open it in?

[Adam Topaz]

I'm actually not sure it's a firefox thing now...

[Adam Topaz]

one sec.

[Adam Topaz]

(My OS is arch btw.)

[Adam Topaz]

Okay, yeah it seems to only be an issue on firefox, for me at least.

[Adam Topaz]

I would guess the issue should go here:
https://github.com/leanprover-community/leanprover-community.github.io

[Rob Lewis]

The issue should go to https://github.com/leanprover-community/doc-gen but I wouldn't expect a fix. My wild guess is FIrefox is scrolling the page to the anchor before it loads the CSS for the header bar and not adjusting.