## Stream: math-comp analysis

### Topic: Locally Compact notation

#### Zachary Stone (Feb 09 2022 at 15:45):

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

1. `forall A, D (globally A) = compact A`
2. `[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: Jun 22 2024 at 15:01 UTC