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: Feb 09 2023 at 02:02 UTC