The problem I'm working through now is attempting to develop a definition of compact such that `[locally compact]`

makes sense. Formally, I need a definition `D`

such that

`forall A, D (globally A) = compact A`

`[locally D (globally A)] = forall x, A x -> exists U, compact U /\ nbhs x U`

I made what I thought was partial progress, with

```
Definition filter_compact (G : (set (set X))) := forall (F : set (set X)),
ProperFilter F -> F `=>` G -> G `#` globally (cluster F).
```

and it's quite straightforward to prove that `filter_compact (globally A) = compact A`

. However `[locally (filter_compact (globally A))]`

seems unhelpful. I'm wondering if anyone has encountered this before? Alternatively, I have a hunch that because compactness is a "second order" property (in the sense that it involves a quantifier over sets not points), this is hopeless. Any help you all can offer would be much appreciated.

Last updated: Sep 28 2023 at 10:01 UTC