The connected Vietoris powerlocale (Q1030196)

The paper presents an investigation into topos-valid, point free constructive analysis, with as main part the study of a new powerlocale. Starting from the Vietoris powerlocale \({V}X\) of \textit{P. T. Johnstone} in [in: Continuous lattices and their applications, Proc. 3rd Conf., Bremen/Ger. 1982, Lect. Notes Pure Appl. Math. 101, 155--180 (1985; Zbl 0581.54005)], which is a localic counterpart to the Vietoris hyperspace, the author defines a sublocale \({V^{c}}X\) whose points correspond to the weakly semifitted sublocales of \(X\) that are strongly connected. It has nice properties such as the existence of product maps by which it follows that the product of two such sublocales is again strongly connected and the fact that over the reals its points are just the compact intervals. Application to the point-free real line \(\mathbb{R}\) gives a choice free constructive version of the Intermediate Value Theorem and Rolle's theorem, both of which are related to connectedness.