The connected Vietoris powerlocale

摘要

The connected Vietoris powerlocale is defined as a strong monad V~c on the category ofrnlocales. V~cX is a sublocale of Johnstone's Vietoris powerlocale V X, a localic analogue ofrnthe Vietoris hyperspace, and its points correspond to the weakly semifitted sublocales of Xrnthat are "strongly connected". A product map × : V~cX × V~cY → V~c(X × Y) shows thatrnthe product of two strongly connected sublocales is strongly connected. If X is locallyrnconnected then V~cX is overt. For the localic completion Y of a generalized metric space Y,rnthe points of V~cY are certain Cauchy filters of formal balls for the finite power set FYrnwith respect to a Vietoris metric.rnApplication to the point-free real line R gives a choice-free constructive version of thernIntermediate Value Theorem and Rolle's Theorem.rnThe work is topos-valid (assuming natural numbers object). V~c is a geometric construction.