Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-geometry differential-topology digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity group-theory 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 infinity integration-theory k-theory kan lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monoidal monoidal-category-theory morphism motives motivic-cohomology newpage nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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 subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

    More about the constructive versions.

    • 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 ff 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 BB had no maximum, then {(,b):bB}\{(-\infty, b): b \in B\} is an open covering of BB, hence has a finite subcovering (,b 1),,(,b n)(-\infty, b_1), \ldots, (-\infty, b_n) where we arrange b 1<<b nb_1 \lt \ldots \lt b_n. But b nBb_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!