Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeNov 9th 2015
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSome remarks and a reference to finish later at [[extreme value theorem]]. But I need to learn more about semicontinuous maps on locales.

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

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexMore about the constructive versions.

   More about the constructive versions.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhat is the intended meaning of "occupied space"? I'm not familiar with that term as distinct from "inhabited".

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

4. • CommentRowNumber4.
   • CommentAuthorspitters
   • CommentTimeNov 17th 2016
   • PermaLink
   Author: spitters
   Format: MarkdownItexOccupied has been coined by Paul Taylor in the context of [[abstract stone duality]]. E.g. in [a lambda calculus for real analysis](http://www.paultaylor.eu/ASD/lamcra/).

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

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeNov 19th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't suppose you could repeat the definition in standard language?

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

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeNov 19th 2016
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI 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 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’.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2017
   • (edited May 15th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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.)

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

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 15th 2017
   • (edited May 15th 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexForgive 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItex> 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 15th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexOkay, thanks -- looks good now!

    Okay, thanks – looks good now!