Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Some remarks and a reference to finish later at extreme value theorem. But I need to learn more about semicontinuous maps on locales.
More about the constructive versions.
What is the intended meaning of “occupied space”? I’m not familiar with that term as distinct from “inhabited”.
Occupied has been coined by Paul Taylor in the context of abstract stone duality. E.g. in a lambda calculus for real analysis.
I don’t suppose you could repeat the definition in standard language?
I wrote ‘occupied’ last year, probably because Taylor treats being occupied as more fundamental for compact spaces than being inhabited. Classically, the two concepts are equivalent. It is perhaps inappropriate to use terminology from ASD when discussing constructive pointwise topology, since that is not a model of ASD (whereas classical topology and constructive locale theory are, at least if one restricts to locally compact spaces). Technically, it was alright where I put it, which was about the classical theory, but there's little point to using it there; and if I don't follow up on it where there would be a point (in a constructive context), then I probably shouldn't use it at all.
This is a long-winded way of saying that you’re right, Mike, and I've changed it to ‘inhabited’.
I have added statement and proof of the standard version of the extreme value theorem.
(Of course the proof is the same for the more general case, but I want to have the classical statement on the page.)
Forgive me for saying so, but the end of the proof reads a little strangely: “Finally by continuity of $f$ it needs to be a single closed interval”. (Justification?)
I suppose that one could say the image is also connected, hence it is a (closed) interval. But this is not how most proofs go. More usual is an argument like this: if the image $B$ had no maximum, then $\{(-\infty, b): b \in B\}$ is an open covering of $B$, hence has a finite subcovering $(-\infty, b_1), \ldots, (-\infty, b_n)$ where we arrange $b_1 \lt \ldots \lt b_n$. But $b_n \in B$ belongs to none of the sets, contradicting the fact they form a covering.
I suppose that one could say the image is also connected, hence it is a (closed) interval.
That’s what I had in mind. I have expanded and merged. Please have a look.
Okay, thanks – looks good now!
1 to 10 of 10