I simply meant that (to me, anyway) the etymology of “overt” might serve to remind one that preservation of *opens* (under appropriate quantification) is taken to be primary. The rest of what you say is obviously true.

It's not the overt characterization but the *dual*-overt characterization; compact spaces are dual to overt spaces. But I believe that it predates overtness anyway.

I'd call it a quantifier characterization. If you have some proposition with free variables that stand for points in topological spaces, such that the truth set of the proposition is open in the product space, and you universally quantify one of the variables, then is the truth set still open? If the variable that you quantified over stood for a point in a compact space, then Yes. (And only a compact space will guarantee that the answer is Yes no matter what the rest of the details are.)

Escardó attributes this to Nachbin. But once you think of it, the proof is very follow-your-nose, especially if you already know the closed-projection characterization of compactness.

]]>I wouldn’t necessarily call it “Escardo’s characterization of compactness”. Just because it’s in his paper doesn’t mean it originated with him. (I’m not sure who should be credited, but in any case I think it might better be called something like “overt characterization of compactness”.)

]]>Thanks that you are looking into this.

After your request in the other thread I had already included an informal pointer here.

But the proper way to do this is, of course. to add a decent Proposition-environment to *compact space* of the form

```
+-- {: .num_defn #EscardoCharacterizationOfCompactness}
###### Proposition
**(Escardo's characterization of compactness)**
A topological space $X$ is compact precisely if...
(...)
=--
+-- {: .proof}
###### Proof
(...)
=--
```

and then link to that from the entry *overt space* by typing

```
Notice that (by [this Prop.](compact+space#EscardoCharacterizationOfCompactness)) a [[topological space]] is _[[compact]]_ if an olny if ...
```

You wanna try to do that edit? It would be a nice service to the community!

]]>Recall that a topological space X is compact if and only if, for every other space Y and any open subspace U of X×Y, the subspace

∀XU={b:Y|∀a:X,(a,b)∈U}

is open in Y."

This was not obvious to me. I asked about it on compact spaces page and Todd said this is proven in escardo 09, lemma 4.3. Can we add a pointer here, or otherwise make it easier to understand this fact?

escardo 09: https://www.cs.bham.ac.uk/~mhe/papers/compactness-submitted.pdf ]]>

Replace ‘subset’ with ‘subspace’ for generality’s sake (except in one case where the specificity was proper).

]]>I added a link to topological locale.

]]>Added to *overt space* two examples: locales induced by topological spaces and spectra of commutative rings in which nilpotency is decidable. (I’ll add details of the spectrum example later.)

At overt space there was a remark that since the definition quantifies over “spaces”, the overtness of a single space might depend on the general meaning chosen for “space”, but that no example was known to the author. I added an example involving synthetic topology, which may not be quite what the author of that remark was thinking of, but which I think is interesting.

]]>