The Connected Vietoris Powerlocale

Steven Vickers

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
196 Downloads (Pure)


The connected Vietoris powerlocale is defined as a strong monad Vc on the category of locales. VcX is a sublocale of Johnstone's Vietoris powerlocale VX, a localic analogue of the Vietoris hyperspace, and its points correspond to the weakly semifitted sublocales of X that are “strongly connected”. A product map ×:VcX×VcY→Vc(X×Y) shows that the product of two strongly connected sublocales is strongly connected. If X is locally connected then VcX is overt. For the localic completion of a generalized metric space Y, the points of are certain Cauchy filters of formal balls for the finite power set with respect to a Vietoris metric. Application to the point-free real line gives a choice-free constructive version of the Intermediate Value Theorem and Rolle's Theorem. The work is topos-valid (assuming natural numbers object). Vc is a geometric construction
Original languageEnglish
Pages (from-to)1886-1910
Number of pages25
JournalTopology and its Applications
Issue number11
Publication statusPublished - 15 Jun 2009


  • Geometric logic
  • Intermediate Value Theorem
  • Rolle
  • Hyperspace
  • Locale


Dive into the research topics of 'The Connected Vietoris Powerlocale'. Together they form a unique fingerprint.

Cite this