Stream: math-comp analysis

Topic: Locally Compact notation

view this post on Zulip 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: Sep 28 2023 at 10:01 UTC