Definition of compactness using filter

Stream: maths

[Jiatong Yang]

I can't understand the def of compactness in mathlib. Can anyone give a short proof of the equivalence between this and the usual "finite covering" def?
"A set s is compact if for every nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a."

[Junyan Xu]

The equivalence is docs#is_compact_iff_finite_subcover.

[Jiatong Yang]

I'm sorry. Is there a more mathematical proof? :rolling_on_the_floor_laughing:

[Patrick Massot]

Jiatong, the docstring you quote is confusing because it breaks the abstraction barrier of the implementation of filters in "that contains s". It would be much better to say that f as a generalized set is contained in s, and this is indeed much closer to how the actual definition is stated.

[Jiatong Yang]

I can now use filter to describe some limit procedures, but when I am given a filter, I don't know what to do to use it.

[Patrick Massot]

Maybe watching https://icerm.brown.edu/video_archive/?play=2899 could help

[Kevin Buzzard]

@Jiatong Yang setting up topology using filters is a really cool trick but if you don't want a filter then you probably never need to deal with them. Just because the internal implementation of something uses filters this doesn't matter to an end user, who can just use the API (ie the theorems).

[Anatole Dedecker]

Maybe it helps to think about what the statement looks like when applied to the whole space. In the topology library we like to make definitions about sets, but it is often harder to parse. Here, this really just means "a topological space $X$ is compact iff each nontrivial filter on $X$ has a cluster point" (docs#cluster_pt)

[Anatole Dedecker]

Here is a mathematical proof. We'll use the dual characterization of compactness (with intersections of closed sets), and the fact that cluster points of a filter $\mathcal{F}$ are exactly the elements of $\bigcap_{A\in\mathcal{F}}\bar{A}$.

• First, assume $X$ is compact, and let $\mathcal{F}$ be a nontrivial filter on $X$. By contradiction, assume that $\mathcal{F}$ has no cluster point, i.e $\bigcap_{A\in\mathcal{F}}\bar{A} = \varnothing$. Since $X$ is compact, that gives a finite set $J \subseteq\mathcal{F}$ with $\bigcap_{A\in J}\bar{A} = \varnothing$ hence $\varnothing=\bigcap_{A\in J} A\in\mathcal{F}$ so $\mathcal{F}$ is trivial, contradiction.
• Second, assume $X$ is "filter-compact", and let $(A_i)_{i\in I}$ be a family of closed sets of $X$ with $\bigcap_{i\in I} A_i = \varnothing$. By contradiction, assume that for all finite $J\subseteq I$, $\bigcap_{i\in J} A_i \neq \varnothing$. Then the filter $\mathcal{F}$ generated by $\{A_i\}_{i\in I}$ is nontrivial, which gives that $\varnothing\ne\bigcap_{A\in\mathcal{F}}\bar{A}\subseteq\bigcap_{i\in I}\bar{A_i}=\bigcap_{i\in I} A_i = \varnothing$, which is a contradiction

[Anatole Dedecker]

(I'm not claiming this is the way it's done in mathlib, but this is the proof I know)

[Jiatong Yang]

Thank you very much! I didn't know that equivalent characterization of cluster pts :joy: .