Questions tagged [overt-spaces]
Overtness is the lattice dual of compactness in various forms of constructive topology and analysis, where related ideas are also called "located" (constructive analysis), "recursively enumerable" (computable analysis), "open" (locale theory) or "positive" (formal topology).
7
questions
55
votes
3
answers
3k
views
Duality between compactness and Hausdorffness
Consider a non-empty set $X$ and its complete lattice of topologies
(see also this thread).
The discrete topology is Hausdorff. Every topology that is finer than a Hausdorff topology is also ...
- 1,691
25
votes
7
answers
4k
views
A topological concept dual to compactness
We say that a subset A in a topological space X is anti-compact if every covering of A by closed sets has a finite subcover. Clearly if X is Hausdorff then all anti-compact subsets of X are finite. ...
- 351
22
votes
5
answers
3k
views
Intermediate value theorem on computable reals
Wikipedia says that the intermediate value theorem “depends on (and is actually equivalent to) the completeness of the real numbers.” It then offers a simple counterexample to the analogous ...
- 595
14
votes
3
answers
1k
views
Is there a universal property characterizing the category of compact Hausdorff spaces?
This is in some sense a follow up to the question asked here Properties of the category of compact Hausdorff spaces
To clarify: The category $\text{Prof}$ of profinite sets sits inside the category $\...
- 1,823
12
votes
2
answers
548
views
Is the Intermediate Value Theorem strictly stronger than LLPO?
(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.)
By LLPO, I mean the statement that ...
- 4,752
5
votes
4
answers
645
views
What does overtness mean for metric spaces?
Original question:
For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed as a property dual to compactness. So is there a similar ...
- 1,803
5
votes
2
answers
862
views
What is the status of the extreme value theorem in forms of constructive mathematics, such as Smooth Infinitesimal Analysis?
In certain intuitionistic frameworks the extreme value theorem cannot be proved. Depending on the exact framework, counterexamples can be constructed as well; see for example pp. 294-295 in
Troelstra,...
- 14.9k