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

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

nLab > Latest Changes: Fan theorem

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeAug 8th 2010

    I wrote fan theorem a while back but I never got around to announcing (or finishing what I wanted to do with it, but that’s OK).

    • CommentRowNumber2.
    • CommentAuthorspitters
    • CommentTimeAug 13th 2014

    I quickly added a reference to sheaf models since we were discussing it on the HoTT-list. The page seems to need some more work.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2018

    Topological invariance of Bishop-compactness implies the fan theorem.

    diff, v16, current

  4. Added a brief warning that the equivalence with the existence of a class of kontinuous functions might need dependent choice. At least Frank’s nice paper uses it. I can’t check right now whether we could eliminate its use.

    diff, v17, current

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJul 13th 2018

    Thanks, that’s interesting. I guess at least we can say that the existence of a class of kontinuous functions implies that “dependent choice implies the fan theorem”, which I suppose is a taboo although a slightly unusual one, so it suffices to conclude that a class of kontinuous functions cannot be proven to exist.

  6. “Uselessness”?

    Anonymous

    diff, v18, current

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 27th 2019

    Hm. Well, “uselessness” may be provocative, but I don’t think it should simply be expunged without some discussion, especially by an “anonymous” source. Renaming it “Importance” simply gainsays the point that was trying to be made. I’m rolling back.

    • CommentRowNumber8.
    • CommentAuthoratmacen
    • CommentTimeJun 27th 2019

    FWIW, I don’t understand the use of “uselessness”. The section seems to be saying it’s practically necessary for “point-wise” analysis. (I have very weak grasp of what all this means though.) Maybe it meant “Uselessness in Point-free Analysis” or something?

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 27th 2019

    re-worded “pointless approaches” to “point-free approaches”, for otherwise it’s pointless

    diff, v20, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJun 27th 2019

    added some more hyperlinks, and a floating TOC. Wanted also to bring the references into more canonical formatting, so that for instance one might know what “Waaldijk’s example” refers to, but then didn’t

    diff, v20, current

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 27th 2019

    Do we want the first person “I” on this page, e.g., “I need to figure out…”? I guess this is from the time Toby was writing pages on constructive mathematics by himself. But if it’s a concept worth including on the nLab it shouldn’t be personalised.

    Presumably we’ll see the rise of HoTT approaches to analysis. There’s a HoTTEST talk

    • Thierry Coquand, A survey of constructive models of univalence

    I will try to survey what is known at this stage about constructive models of univalence, and then some metatheoretical applications. Some of these are: proof theoretic strength of the univalence axiom (with HITs), and consistency of univalence with continuity principle and fan theorem, and independence of the axiom of countable choice.

    Is there much work going on here? I see

    • Auke Booij, Constructive analysis in univalent type theory, (slides)
    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 27th 2019

    Yes, the use of first person should be changed. Somebody might want to go through the whole entry and professionalize the presentation a little.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJun 27th 2019

    Regarding #6, I think the word “Importance” as a section header could be interpreted to just label a discussion of its importance and/or lack thereof, rather than an assertion that it is important. But I agree it’s confusing. How about calling the section “Analysis without the fan theorem”, since it’s a discussion of how possible such a thing is?

    diff, v21, current

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJun 27th 2019

    Also I made the reference to Waaldjk a bit more specific, though it would be even better to have a hyperlink. I suppose someone sufficiently motivated could create kontinuous function…

    • CommentRowNumber15.
    • CommentAuthorMarkSaving
    • CommentTimeJun 16th 2020
    I noticed that the page claims that what it calls the "classical fan theorem" contradicts the continuity principle. This is not the case - in fact, the "classical fan theorem" is actually a consequence of (one version of) the continuity principle + the (decidable) fan theorem and is therefore intuitionistically valid.. See e.g. Dummett's "Elements of Intuitionism". I assume that the author was thinking of unrestricted Bar Induction which does contradict even the weakest version of the continuity principle.

    Also, I found an article which states that the Fan Theorem is not equivalent to the Heine-Borel Theorem (i.e. the compactness of the interval [0, 1]) in every topos, which again contradicts the nLab page.

    Moerdijk, Ieke. “Heine-Borel Does Not Imply the Fan Theorem.” Journal of Symbolic Logic, vol. 49, no. 2, 1984, pp. 514–519., doi:10.2307/2274182

    I intend to modify the page if I see no objections here.

1 to 15 of 15

  1.