Zulip Chat Archive

Stream: Is there code for X?

Topic: Characterization of closed subspace


view this post on Zulip Heather Macbeth (Dec 21 2020 at 18:42):

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

view this post on Zulip Adam Topaz (Dec 21 2020 at 18:59):

There's docs#mem_closure_iff_ultrafilter

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:00):

And docs#is_closed.closure_eq

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:01):

Actually you can probably just use docs#is_closed_iff_cluster_pt

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 19:03):

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?

view this post on Zulip Heather Macbeth (Dec 21 2020 at 19:03):

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.

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 19:04):

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.

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:04):

I have the same issue

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:05):

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

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 19:06):

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

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:07):

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

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:07):

one sec.

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:08):

(My OS is arch btw.)

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:09):

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

view this post on Zulip Adam Topaz (Dec 21 2020 at 19:14):

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

view this post on Zulip Rob Lewis (Dec 21 2020 at 19:22):

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.


Last updated: May 16 2021 at 05:21 UTC