## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTobyBartels
• CommentTimeNov 9th 2015

Some remarks and a reference to finish later at extreme value theorem. But I need to learn more about semicontinuous maps on locales.

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeNov 17th 2016

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeNov 17th 2016

What is the intended meaning of “occupied space”? I’m not familiar with that term as distinct from “inhabited”.

• CommentRowNumber4.
• CommentAuthorspitters
• CommentTimeNov 17th 2016

Occupied has been coined by Paul Taylor in the context of abstract stone duality. E.g. in a lambda calculus for real analysis.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeNov 18th 2016

I don’t suppose you could repeat the definition in standard language?

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeNov 19th 2016

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

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMay 15th 2017
• (edited May 15th 2017)

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

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeMay 15th 2017
• (edited May 15th 2017)

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.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMay 15th 2017

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.

• CommentRowNumber10.
• CommentAuthorTodd_Trimble
• CommentTimeMay 15th 2017

Okay, thanks – looks good now!