Localic Tychonoff theorem
= 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.