Skip to main content
Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
isaccepted:yes
hasaccepted:no
inquestion:1234
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*.example.com"
Saves in:saves
Status closed:yes
duplicate:no
migrated:no
wiki:no
Types is:question
is:answer
Exclude -[tag]
-apples
For more details on advanced search visit our help page
Results tagged with
Search options answers only not deleted user 1176

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).

20 votes

Intermediate value theorem on computable reals

I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose $f$ is continuous and computable on $[a,b]$ and $f(a) \cdot f(b) < 0$. We must be careful to distinguish bet …
Andrej Bauer's user avatar
  • 48.8k
4 votes

What does overtness mean for metric spaces?

To conjure up a non-overt space we must change slightly the definition of topology, since even inuitionistically every space is overt, so long as every union of opens is open. Let $\Sigma$ be the Sier …
Andrej Bauer's user avatar
  • 48.8k
65 votes

A topological concept dual to compactness

When looking for a dual concept we should be careful not to be tricked by a shallow symmetry. I will not comment on your definition of anti-compactness. Instead I would like to explain what the "true" …
Andrej Bauer's user avatar
  • 48.8k
17 votes

Duality between compactness and Hausdorffness

Hausdorff is dual to discrete. Compact is dual to overt. A space $X$ is Hausdorff if and only if the diagonal $\Delta_X = \{(x,x) \mid x \in X\}$ is closed in $X \times X$. A space $X$ is discrete if …
Andrej Bauer's user avatar
  • 48.8k