## Stream: Is there code for X?

### Topic: Characterization of closed subspace

#### 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

#### Adam Topaz (Dec 21 2020 at 19:01):

Actually you can probably just use docs#is_closed_iff_cluster_pt

#### 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?

#### Heather Macbeth (Dec 21 2020 at 19:03):

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 (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.

#### Adam Topaz (Dec 21 2020 at 19:04):

I have the same issue

#### 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...)

#### 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?

#### Adam Topaz (Dec 21 2020 at 19:07):

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

one sec.

#### Adam Topaz (Dec 21 2020 at 19:08):

(My OS is arch btw.)

#### Adam Topaz (Dec 21 2020 at 19:09):

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

#### 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

#### 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