Compact locale

A locale is compact when every directed family of opens whose join is $1$ contains $1$. Equivalently every open cover has a finite subcover. The truth-valued test $a\mapsto [a=1]$ is a preframe homomorphism exactly when the locale is compact.

An arbitrary product of compact locales is compact. Finite products correspond to preframe tensor products, whose compactness follows by tensoring the top tests. An arbitrary product is obtained by the filtered colimit of finite frame coproducts; the eventual-top test proves that filtered colimits preserve compactness. No choice of points is required.