 Localic Tychonoff theorem

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.